The technology of formal software verification has made spectacular advances, but how much does it actually benefit the development of practical software? Considerable disagreement remains about the practicality of building systems with mechanically-checked proofs of correctness. Is this prospect confined to a few expensive, life-critical projects, or can the idea be applied to a wide segment of the software industry? To help answer this question, the present survey examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.

Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: a test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of Design by Contract, as available in Eiffel, and exploiting a feature of modern program-proving tools based on “Satisfiability Modulo Theories” (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation. We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and Design by Contract, hold significant promise to address some of the challenges of program testing, software maintenance and Automatic Program Repair.

Software engineering concepts and processes are worthy of formal study; and yet we seldom formalize them. This "research ideas" article explores what a theory of software engineering could and should look like. Software engineering research has developed formal techniques of specification and verification as an application of mathematics to specify and verify systems addressing needs of various application domains. These domains usually do not include the domain of software engineering itself. It is, however, a rich domain with many processes and properties that cry for formalization and potential verification. This article outlines the structure of a possible theory of software engineering in the form of an object-oriented model, isolating abstractions corresponding to fundamental software concepts of project, milestone, code module, test and other staples of our field, and their mutual relationships. While the presentation is only a sketch of the full theory, it provides a set of guidelines for how a comprehensive and practical Theory of Software Engineering should (through an open-source community effort) be developed.

Among areas of software engineering where AI techniques – particularly, Large Language Models – seem poised to yield dramatic improvements, an attractive candidate is Automatic Program Repair (APR), the production of satisfactory corrections to software bugs. Does this expectation materialize in practice? How do we find out, making sure that proposed corrections actually work? If programmers have access to LLMs, how do they actually use them to complement their own skills? To answer these questions, we took advantage of the availability of a program-proving environment, which formally determines the correctness of proposed fixes, to conduct a study of program debugging with two randomly assigned groups of programmers, one with access to LLMs and the other without, both validating their answers through the proof tools. The methodology relied on a division into general research questions (Goals in the Goal-Query-Metric approach), specific elements admitting specific answers (Queries), and measurements supporting these answers (Metrics). While applied so far to a limited sample size, the results are a first step towards delineating a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs. These results caused surprise as compared to what one might expect from the use of AI for debugging and APR. The contributions also include: a detailed methodology for experiments in the use of LLMs for debugging, which other projects can reuse; a fine-grain analysis of programmer behavior, made possible by the use of full-session recording; a definition of patterns of use of LLMs, with 7 distinct categories; and validated advice for getting the best of LLMs for debugging and Automatic Program Repair.

In industrial practice, requirements are an indispensable element of any serious software project. In the academic study of software engineering, requirements are one of the heavily researched subjects. And yet requirements engineering, as practiced in industry, makes shockingly sparse use of the concepts propounded in the requirements literature. The present paper starts from an assumption about the causes for this situation and proposes a remedy to redress it. The posited explanation is that change is the major factor affecting the practical application of even the best-intentioned requirements techniques. No sooner has the ink dried on the specifications than the system environment and stakeholders' views of the system begin to evolve. The proposed solution is a requirements engineering method, called UOOR, which unifies many known requirements concepts and a few new ones in a framework entirely devised to accommodate and support seamless change throughout the project lifecycle. The method encompasses the commonly used requirements techniques, namely, scenarios, and integrates them into the seamless software development process. The work presented here introduces the notion of seamless requirements traceability, which relies on the propagation of traceability links, themselves based on formal properties of relations between project artifacts. As a proof of concept, the paper presents a traceability tool to be integrated into a general-purpose IDE that provides the ability to link requirements to other software project artifacts, display notifications of changes in requirements, and trace those changes to the related project elements. The UOOR approach is not just a theoretical proposal but has been designed for practical use and has been applied to a significant real-world case study: Roborace, a competition of autonomous racing cars.

A re-construction of the fundamentals of programming as a small mathematical theory (PRISM) based on elementary set theory. Highlights: ∙ Zero axioms. No properties are assumed, all are proved (from standard set theory). ∙ A single concept covers specifications and programs. ∙ Its definition only involves one relation and one set. ∙ Everything proceeds from three operations: choice, composition and restriction. ∙ These techniques suffice to derive the axioms of classic papers on the "laws of programming" as consequences and prove them mechanically. ∙ The ordinary subset operator suffices to define both the notion of program correctness and the concepts of specialization and refinement. ∙ From this basis, the theory deduces dozens of theorems characterizing important properties of programs and programming. ∙ All these theorems have been mechanically verified (using Isabelle/HOL); the proofs are available in a public repository. This paper is a considerable extension and rewrite of an earlier contribution [arXiv:1507.00723]

Vibe coding, the much-touted use of AI techniques for programming, faces two overwhelming obstacles: the difficulty of specifying goals ("prompt engineering" is a form of requirements engineering, one of the toughest disciplines of software engineering); and the hallucination phenomenon. Programs are only useful if they are correct or very close to correct. The solution? Combine the creativity of artificial intelligence with the rigor of formal specification methods and the power of formal program verification, supported by modern proof tools.

Automatic Program Repair (APR) is a brilliant idea: when detecting a bug, also provide suggestions for correcting the program. Progress towards that goal is hindered by the absence of a common frame of reference for the multiplicity of APR ideas, methods, tools, programming languages and environments. Bugfix is an effort at providing such a framework: a standardized set of notations, tools and interfaces, as well as a database of bugs and fixes, for use by the APR research community to try out ideas and compare results. The most directly visible component of the Bugfix effort is the Bugfixlanguage, a human-readable formalism making it possible to describe elements of the following kinds: a bug (described abstractly, for example the permutation of two arguments in a call); a bug example (an actual occurrence of a bug, in a specific code written in a specific programming language, and usually recorded in some repository); a fix (a particular correction of a bug, obtained for example by reversing the misplaced arguments); an application (an entity that demonstrates how a actual code example matches with a fix); a construct (the abstract description of a programming mechanism, for example a “while” loop, independently of its realization in a programming language; and a language (a description of how a particular programming language includes certain constructs and provides specific concrete syntax for each of them – for example Java includes loop, assignment etc. and has a defined format for each of them). A JSON API provides it in a form accessible to tools. Bugfix includes a repository containing a considerable amount of bugs, examples and fixes. Note: An early step towards this article was a short contribution (Ref [1]) to the 2024 ICSE. The present text reuses a few elements of introduction and motivation but is otherwise thoroughly reworked and extended.

In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments: an invariant, for functional properties (ignoring termination); and a variant, for termination (ignoring functional properties). A single and simple definition is possible, removing this split. A loop is just the limit (a variant of the reflexive transitive closure) of a Noetherian (well-founded) relation. To prove the loop correct there is no need to devise an invariant and a variant; it suffices to identify the relation, yielding both partial correctness and termination. The present note develops the (small) theory and applies it to standard loop examples and proofs of their correctness.

Testing processes usually aim at high coverage, but loops severely limit coverage ambitions since the number of iterations is generally not predictable. The most common solution is extreme: it limits its aims to achieving branch coverage, which only considers loop executions that iterate the body either once or not at all. This approach misses bugs that only arise after two or more iterations. To achieve more meaningful coverage, testing strategies may unroll loops, iterating them up to n times for some n greater than one, chosen pragmatically in consideration of the available computational power. While loop unrolling is a standard part of compiler optimization techniques, its use in testing is less common. Part of the reason is that the concept, while seemingly intuitive, lacks a generally accepted and precise specification. The present article provides a formal definition and a set of formal properties of unrolling. All the properties have mechanically been proved correct (through the Isabelle proof assistant). Using this definition, we have applied an unrolling strategy to an automated testing framework. The results indicate how many bugs the usual approach misses by limiting itself to branch coverage, analyzing the benefits (in number of detected bugs) and costs of successive unrolling levels. They provide important factual information on the merits of including unrolling in testing strategies and coverage measurement.

Techniques of Automatic Program Repair (APR) have the potential of thoroughly facilitating the task of producing quality software. After a promising start, however, progress in making APR practical has been hindered by the lack of a common framework to support the multiplicity of APR ideas and tools, and of target programming languages and environments. In this position paper we outline a general framework to enable the APR community to benefit from each other's advances, in particular through a standard language for describing bugs and their fixes. Such a common framework - which is also applicable to work on fault seeding - could be a tremendous benefit to researchers and developers of Interactive Development Environments (IDEs) who are working to make APR an effective part of the software developer's practical experience.

Techniques to achieve various forms of test coverage, such as branch coverage, typically do not iterate loops; in other words, they treat a loop as a conditional, executed zero or one time. Existing work by the author and collaborators produces test suites guaranteeing full branch coverage. More recent work has shown that by unrolling loops the approach can find significantly more bugs. The present discussion provides the theoretical basis and precise definition for this concept of unrolling.

Automatic program repair usually relies heavily on test cases for both bug identification and fix validation. The issue is that writing test cases is tedious, running them takes much time, and validating a fix through tests does not guarantee its correctness. The novel idea in the Proof2Fix methodology and tool presented here is to rely instead on a program prover, without the need to run tests or to run the program at all. Results show that Proof2Fix automatically finds and fixes significant historical bugs.

Class invariants -- consistency constraints preserved by every operation on objects of a given type -- are fundamental to building, understanding and verifying object-oriented programs. For verification, however, they raise difficulties, which have not yet received a generally accepted solution. The present work introduces a proof rule meant to address these issues and allow verification tools to benefit from invariants. It clarifies the notion of invariant and identifies the three associated problems: callbacks, furtive access and reference leak. As an example, the 2016 Ethereum DAO bug, in which $50 million were stolen, resulted from a callback invalidating an invariant. The discussion starts with a simplified model of computation and an associated proof rule, demonstrating its soundness. It then removes one by one the three simplifying assumptions, each removal raising one of the three issues, and leading to a corresponding adaptation to the proof rule. The final version of the rule can tackle tricky examples, including "challenge problems" listed in the literature.

Techniques to achieve various forms of test coverage, such as branch coverage, typically do not iterate loops; in other words, they treat a loop as a conditional, executed zero or one time. Existing work by the author and collaborators produces test suites guaranteeing full branch coverage. More recent work has shown that by "unrolling" loops the approach can find significantly more bugs. The present discussion provides the theoretical basis and precise definition for this concept of unrolling. While initially motivated by the need to improve standard test coverage practices (which execute loop bodies only once), to better testing coverage, the framework presented here is applicable to any form of reasoning about loops.

MCDC, for "Modified Condition/Decision Coverage", is a test coverage criterion recommended in several important industrial software safety standards. The intuition behind MCDC is that it should be more effective than industry's default coverage criterion, branch coverage, since it uses a finer-grain decomposition of program conditions. Manually generating MCDC-compliant test suites is, however, tedious and error-prone; there is, as a result, little empirical evidence of whether that intuition holds up in practice. Does MCDC really provide enough of an advantage over branch coverage to justify the extra work and longer test runs? To help answer this question, the present work takes advantage of verification technology that combines tests and proofs, based on the Auto-Proof program verifier. For each decision point in the program, the approach proceeds in four steps. First, compute a set of conditions that satisfy MCDC. Then, inject into the program, for each combination, an incorrect instruction (a "seeded contradiction" in the terminology of previous work). Next, apply the prover to verify the instrumented program; the prover naturally fails, but in the process it produces a set of counterexamples covering all the combinations. Finally, turn this result into a directly usable test suite-guaranteed by construction to satisfy the MCDC criterion. The results, on a significant set of example programs, yield insights on how MCDC coverage compares to branch coverage and adaptive random testing when trying to detect faults.

A successful automated program proof is, in software verification, the ultimate triumph. In practice, however, the road to such success is paved with many failed proof attempts. Unlike a failed test, which provides concrete evidence of an actual bug in the program, a failed proof leaves the programmer in the dark. Can we instead learn something useful from it? The work reported here takes advantage of the rich information that some automatic provers internally collect about the program when attempting a proof. If the proof fails, the Proof2Test tool presented in this article uses the counterexample generated by the prover (specifically, the SMT solver underlying the Boogie tool used in the AutoProof system to perform correctness proofs of contract‐equipped Eiffel programs) to produce a failed test, which provides the programmer with immediately exploitable information to correct the program. The discussion presents Proof2Test and the application of the ideas and tool to a collection of representative examples.

On the basis of discussions at the $$2^{nd}$$ edition of the Frontiers on Software Engineering Education workshop, researchers identified challenges brought by the use of AI assistants into computing education. These challenges represent a starting point for the endless road towards effective education of software engineering and computing science in higher education. This paper summarises the challenges and research opportunities that were identified during the heated discussions at the workshop. By the time this paper is read, new works related to AI assistants would have been reported. These works might have either partially or totally addressed the research challenges reported here. If that is the case, then it would have been proven that they were valid research questions. Otherwise, the community should start addressing them shortly. One way or the other, we trust the information provided here may help to raise awareness of the concerns brought by AI assistants into higher computing education.

A paradox of requirements specifications as dominantly practiced in the industry is that they often claim to be object-oriented (OO) but largely rely on procedural (non-OO) techniques. Use cases and user stories describe functional flows, not object types. To gain the benefits provided by object technology (such as extendibility, reusability, reliability), requirements should instead take advantage of the same data abstraction concepts - classes, inheritance, information hiding - as OO design and OO programs. Many people find use cases and user stories appealing because of the simplicity and practicality of the concepts. Can we reconcile requirements with object-oriented principles and get the best of both worlds? This article proposes a unified framework. It shows that the concept of class is general enough to describe not only "objects" in a narrow sense but also scenarios such as use cases and user stories and other important artifacts such as test cases and oracles. Having a single framework opens the way to requirements that enjoy the benefits of both approaches: like use cases and user stories, they reflect the practical views of stakeholders; like object-oriented requirements, they lend themselves to evolution and reuse.