Formalisation and Soundness of Static Verification Algorithms for Imperative Programs (Formalisatie en correctheid van statische verificatiealgoritmes voor imperatieve programma's)

Not only does our software grow larger and more complex, we also become more dependent on it, thus making it all the more necessary to develop tools that assist us in writing correct programs. As a consequence, much research has been done in the field of static verification, i.e. the development of algorithms that analyse source code and determine whether it contains certain kinds of errors. This can range from checking that no null dereferences can occur at runtimeto full functional correctness.Verification algorithms, however, are just as much subject to mistakes. Therefore, it is important to put these algorithms under scrutiny: our trust in software can only be as strong as the confidence we can have in our verification tools. In a first step, we closely examine some existing approaches to verification. More specifically, we fully formalise the verification algorithms and prove their soundness.If we are not willing to trust our software nor our verification algorithms, one can wonder why we should trust our formalisations and proofs. For this reason, we also provide full Coq implementations of all verification algorithms we consider, and, for most of them, machine check the soundness proofs.This thesis is divided into two parts. In the first part, we discuss verification condition generation. This approach consists of deriving a logical formula (called verification condition) from a program's source code, whose validity implies the correctness of the program with respect to given specifications. Three such algorithms are investigated, namely the strongest postcondition, the weakest liberal precondition and the weakest precondition. Extra attention is given to the weakest precondition algorithm. In its classic form, it produces a verification condition that grows exponentially with respect to the size of the program. An alternative formulation is available which generates a verification condition that grows only polynomially, but requires the program to be passive, i.e. to not contain any assignments. Fortunately, it is possible to transform any program into an equivalent passive form.We implement this transformation in Coq as well as the more efficient variant of the weakest precondition algorithm, and we provide fully machine checked proofs that this approach is sound.In the second part of the thesis, we turn our attention to symbolic execution. This approach consists of abstractly interpreting the program in such a way that all possible execution paths are considered simultaneously. Verification succeeds if no errors are encountered during this execution.Based on this technique we develop Featherweight VeriFast, representing the core part of VeriFast, an existing verifier developed at the KU Leuven. Featherweight VeriFast is formally defined as a denotational semantics, but it has been implemented in Coq and is extractable, making it usable as a standalone verifier.Featherweight VeriFast's formalisation is built on top of three abstraction layers. The first layer, the result algebra, allows us to reason about angelic and demonic choices, both needed to express the result of a symbolic execution. The second layer defines operators, composable monadic functions which allow us to elegantly deal with the two kinds of nondeterminism and state in a purely functional setting. The third layer provides basic operators, which together form a domain specific language, abstracting away the details of the result algebra. The symbolic execution, central to Featherweight VeriFast's operation, is then defined in terms of these basic operators. Finally, we also provide a (partially machine checked) soundness proof for Featherweight VeriFast. A last chapter discusses verification automation techniques. Some verifiers, for example VeriFast, require the code to be annotated (with for example routine contracts or loop invariants) to be able to determine a program's correctness. Generating these annotations automatically can dramatically decrease the effort required to verify programs. We discuss and compare three different automation techniques. Lastly, we propose a framework in which automation techniques can be added without compromising the soundness of the verification.1 Introduction 1 1.1 Static Verification Of Imperative Programs 1.2 Overview of Contributions 1.3 Summary I Verification Condition Generation 2 Overview 3 Phase I: From Source to Intermediate Language 13 3.1 BoogiePL 3.2 Source Language 3.2.1 Syntax 3.2.2 Typing 3.2.3 Operational semantics 3.2.4 Modularisation 3.3 Translation 3.3.1 Logical Part 3.3.2 Procedural Part 4 Formal Semantics of the Intermediate Verification Language 4.1 Syntax 4.2 Operational Semantics 4.3 Conclusion 5 Phase II: Generating Verification Conditions 5.1 Hoare Logic 5.2 Strongest Postcondition 5.3 Weakest Liberal Precondition 5.4 Weakest Precondition 5.5 Conclusion 6 Efficient Weakest Preconditions 6.1 Single Assignment Form 6.2 Passification 6.3 EfficientWeakest Preconditions 6.4 Soundness and Size 6.5 Conclusion II Symbolic Execution and Separation Logic 7 Introduction 8 VeriFast Introduction 8.1 Separation Logic 8.1.1 Rationale 8.1.2 Separating Conjunction and Frame Rule 8.2 VeriFast: Hands On 8.2.1 Basics 8.2.2 User Defined Predicates 8.2.3 Recursive User Defined Predicates 8.2.4 List Reversal 8.2.5 Ambiguous Matches 8.3 Related Verification Tools 8.4 Conclusion 9 Featherweight VeriFast 9.1 Small Imperative Language 9.2 Overview 9.3 Result Algebra 9.3.1 Examples 9.3.2 Operations and Axioms 9.3.3 Lemmas 9.4 Operators 9.5 Basic Operators 9.6 Result Algebra Models 9.6.1 Inductive Formulae 9.6.2 Weakest Preconditions 9.7 Operator Lemmas 9.8 Concrete Execution 9.8.1 Formalisation 9.8.2 Shortcomings 9.9 Semiconcrete Execution 9.9.1 Formalisation 9.9.2 Relation with Concrete Execution 9.10 Symbolic Execution 9.10.1 Formalisation 9.10.2 Relation with Semiconcrete Execution 9.10.3 Relation with Concrete Execution 9.11 Conclusion 10 Automation 10.1 General Approach And Rationale 10.2 Working Example 10.3 Auto-open and Auto-close 10.4 Autolemmas 10.5 Shape Analysis 10.6 Comparison 10.7 Conclusion 11 Conclusion and Future Work 11.1 Summary 11.2 Verification Condition Generation vs Symbolic Execution 11.2.1 Similarities 11.2.2 Performance 11.3 RelatedWork 11.3.1 Verification Condition Generation 11.3.2 Symbolic Execution and Separation Logic 11.4 Future Work 11.4.1 Further Formalisation of Verification Condition Generation 11.4.2 Featherweight VeriFast 11.4.3 VeriFast 11.4.4 Reflectionnrpages: 482status: publishe