arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · cs/9906030

SCR3: towards usability of formal methods

M. Chechik
View original source ↗Read source document ↗Export metadata ↓

Abstract

This paper gives an overview of SCR3 -- a toolset designed to increase the usability of formal methods for software development. Formal requirements are specified in SCR3 in an easy to use and review format, and then used in checking requirements for correctness and in verifying consistency between annotated code and requirements. In this paper we discuss motivations behind this work, describe several tools which are part of SCR3, and illustrate their operation on an example of a Cruise Control system.

Explore related subjects

cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

M. Chechik. 1999-06-28. SCR3: towards usability of formal methods. https://arxiv.org/abs/cs/9906030

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Psychological Safety Framework in Pull-based Open Source Projects

Psychological safety (PS) refers to the belief that team members can speak up, ask questions, and make mistakes without fear of negative consequences. Although PS has been studied in traditional software teams, less is known about how it may appear in pull-based open-source software development, where contributors are self-directed and often collaborate voluntarily. This paper introduces a theory-informed framework for understanding how PS may be reflected in pull request (PR) interactions. We investigate the framework through a mixed-methods approach combining repository-based analysis and a survey of OSS contributors. First, we constructed a PS index using nine observable PR interaction indicators extracted from 60,685 PRs across 26 GitHub repositories. Second, we surveyed 57 OSS contributors about their perceived PS and experiences of corresponding PR interactions. All nine surveyed interaction indicators were significantly and positively associated with perceived PS. However, the repository-based index was not significantly associated with survey-reported PS. Contributors' open-ended responses further highlighted the importance of feedback quality, opportunities to participate, and how PR outcomes are interpreted. Together, our framework and mixed-methods findings provide initial insights into how PS may be reflected in PR interactions, highlighting the importance of both PR interaction patterns and contributors' experiences.

cs.SE↗
arXiv2026

Structuring license permissiveness from pairwise comparisons

Licenses are legal instruments that inventors rely upon to protect the technologies they build and regulate how they are used---however, the nature of their authorship and selection implies that how they are interpreted, chosen, and enforced is largely unstructured. In practice, this makes it difficult to compare licenses at scale---when is one license considered more permissive than the other, and when are their terms incomparable to each other? Currently, there is a growing list of licenses that are introduced and used, yet no systematic way to study their relationships. This matters for platforms such as Hugging Face, GitHub, and the Python Package Index, where developers publish or build upon technologies that each have their own licenses. Using large language models (LLMs), we introduce methods for comparing licenses at scale: first, in a pairwise fashion to construct and validate a partial ordering based on permissiveness; and by drawing on existing taxonomies of software licenses. Then, we try to recover the structure with the Bradley-Terry model to see if permissiveness can be judged more cheaply and observe a loss of $\sim$20\%---and classify this loss to feature coverage. The former coupled with model rationale allows us to trace restrictiveness, and the latter allows us to understand license selection as a combination of shared provisions.

cs.SE↗
arXiv2026

Repository and Issue Characteristics of Early GenAI Adopters on GitHub

Generative artificial intelligence (GenAI) has introduced new forms of AI assistance into software development, but less is known about the repositories and issues of early adopters of GenAI tools. We study the repository and issue characteristics of early adopters who state interest in GenAI on their public profiles on GitHub by analyzing 531 early adopters, 100 of their repositories with AI-tool configuration files (ACFs), 100 matched control repositories without ACFs, and 370 issues from the two repository groups. Repositories with ACFs show modest distributional differences in selected README structural characteristics. They contain longer README files with more code blocks and include a license more often, while repositories without ACFs contain more external URLs. The category distributions of the two repository groups show weak evidence of a difference. Once GenAI relatedness is held fixed, we detect no difference in issue Type or Outcome between the two repository groups. Our data, collected from May to August 2025, record how early adopters developed software in Software Engineering 2.0, the stage in which developers use both AI assistants and autonomous AI agents. When these agents become the norm, later studies can compare their data with ours.

cs.SE↗