Related papers: A Tutorial on Using Dafny to Construct Verified So…
Formal verification techniques aim at formally proving the correctness of a computer program with respect to a formal specification, but the expertise and effort required for applying formal specification and verification techniques and…
In recent years, program verifiers and interactive theorem provers have become more powerful and more suitable for verifying large programs or proofs. This has demonstrated the need for improving the user experience of these tools to…
Dafny is a verification-aware programming language that comes with a compiler and static program verifier. However, neither the compiler nor the verifier is proved correct; in fact, soundness bugs have been found in both tools. This paper…
This report presents the Dafny language and verifier, with a focus on describing the main features of the language, including pre- and postconditions, assertions, loop invariants, termination metrics, quantifiers, predicates and frames.…
This paper describes the formal verification of two Turing machines using the program verifier Dafny. Both machines are deciders, so we prove total correctness. They are typical first examples of Turing machines used in any course of…
Formal software verification techniques are widely used to specify and prove the functional correctness of programs. However, nonfunctional properties such as time complexity are usually carried out with pen and paper. Inefficient code in…
Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with…
Formal verification of software is a bit of a niche activity: it is only applied to the most safety-critical or security-critical software and it is typically only performed by specialized verification engineers. This paper considers…
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…
Using large language models (LLMs) to generate source code from natural language prompts is a popular and promising idea with a wide range of applications. One of its limitations is that the generated code can be faulty at times, often in a…
Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally…
Dafny is a verification-aware programming language that allows developers to formally specify their programs and prove them correct. Currently, a Dafny program is compiled in two steps: First, a backend translates the input program to a…
Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to significantly reduce the effort to write verified programs, users…
Formal methods yet advantageous, face challenges towards wide acceptance and adoption in software development practices. The major reason being presumed complexity. The issue can be addressed by academia with a thoughtful plan of teaching…
Formal methods for software correctness are critical to the future of software engineering - and so must be an essential part of software engineering education. Unfortunately, formal methods are often resisted by students due to perceived…
Algorithmic and data refinement are well studied topics that provide a mathematically rigorous approach to gradually introducing details in the implementation of software. Program refinements are performed in the context of some programming…
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications,…
Modern program verifiers use the same uniform program text to both specify and implement programs. The program text is also used to provide the necessary guidance to ensure that the program satisfies its specification. The amount of…
As software becomes more complex and assumes an even greater role in our lives, formal verification is set to become the gold standard in securing software systems into the future, since it can guarantee the absence of errors and entire…
Formal methods provide systematic and rigorous techniques for software development. We strongly believe that they must be taught in computer science curricula. In this paper we present the pedagogic rationale and the concrete implementation…