< Back to previous page
Project
Formalisation and Soundness of Static Verification Algorithms for Imperative Programs
Not only does our software grow larger and more complex, we also becomemore dependent on it, thus making it all the more necessary to develop tools that assist us in writing correct programs. As a consequence, muchresearch 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 nonull dereferences can occur at runtime
to 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 canwonder 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 possibleto 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 threeabstraction 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 kindsof 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.
to 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 canwonder 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 possibleto 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 threeabstraction 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 kindsof 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.
Date:5 Feb 2008 → 13 Dec 2012
Keywords:Specific languages
Disciplines:Applied mathematics in specific fields, Computer architecture and networks, Distributed computing, Information sciences, Information systems, Programming languages, Scientific computing, Theoretical computer science, Visual computing, Other information and computing sciences
Project type:PhD project