Exploring Annotations for Deductive Verification
Sophie Lathouwers is a PhD student in the department Formal Methods and Tools. Promotor is prof.dr. M. Huisman from the faculty of Electrical Engineering, Mathematics and Computer Science.
Waking up to the alarm on your phone, driving to work, sending emails, ordering groceries, playing video games, all of it relies on software. And, we have never been more reliant on software for critical tasks such as in healthcare, banking and self-driving cars. For these critical tasks, it is very important that these systems are safe, reliable and secure. However, building such systems is extremely difficult. It is therefore essential that we provide software developers with tools and techniques to assist them in developing safe, reliable and secure software.
One way to help developers build reliable software is through program verification. We use the term program verification to refer to the verification (conformance evaluation) of programs (executable models). Hence, it covers many different techniques such as model checking, testing, theorem proving, etc. of source code, automata, transition systems, etc. These techniques are used to determine whether a program is correct. The correctness is determined by a formal specification or property that expresses what the program should conform to. For example, one could check type safety, full functional correctness, or termination of a program.
The first part of this thesis focuses on the tools that are currently available for program verification. There are many different tools available and it can be difficult to find the tool that is right for you. We provide a megamodel to distinguish the tools that are available. Moreover, we set up a data set containing many program verification tools that have been categorised according to this megamodel. This provides a concrete point for users where they can explore what kind of program verification tools exist and might be right for them. We also explore the trends that we can see in the different levels of the megamodel.
After exploring the world of program verification, we focus on a specific type of program verification tool namely deductive verifiers. Deductive verifiers require the user to annotate the program with specifications. These specifications express in detail how the program should behave. These specifications as well as the program are then passed to the tool, that will use logic to determine whether the program behaves as expected, i.e. adheres to the specification. This technique is very powerful as it is able to verify programs that may be too difficult when using other techniques. For example, we can reason about concurrent programs that would cause a state-space explosion in many model checking tools. However, while it is powerful and can be used for the verification of functional correctness as well as memory safety, a big drawback of deductive verification is the “specification bottleneck".
The “specification bottleneck" is a term that is used to refer to the process of writing specifications for deductive verifiers. Deductive verifiers require the user to annotate the program with specifications as mentioned before. Aside from specifying the behavior that we are interested in verifying, it often also requires additional specifications to help resolve proof obligations. As a result, the user is required to find and formalise these specifications which requires time and expertise. This limits the application of deductive verification in practice, hence it is called the “specification bottleneck".
This thesis aims to help alleviate the specification bottleneck by investigating specifications for deductive verification. Specifically, this thesis provides three chapters that focus on specifications for deductive verification.
First, we investigate what specifications are typically used to verify programs with deductive verifiers, what they are used for, and how often they occur. This has been done by providing a taxonomy that categorises the specifications. A data set has been set up which contains specifications used by several deductive verifiers. This data is statistically analysed to infer how often different types of specifications are expected to occur. This gives us a better understanding of the specifications that are needed to verify programs. Moreover, we show how this can be used to estimate the impact of specification inference tools.
Next, we survey the existing field of specification inference tools.
While many tools have been proposed, it is difficult to identify the best tools and techniques for specification inference because:
· Many specification inference tools only support a single specification language thereby limiting their impact.
· The tools support different specification languages and use different data sets to evaluate their impact, thereby making it difficult to compare tools.
As a result, it is currently unclear what specifications can be inferred, and what we should focus on for the future. This survey gives an overview of specification inference tools that are currently available. Moreover, we use the taxonomy presented earlier to estimate their impact. Based on this we identify gaps in the current state of the art.
Finally, we propose a tool called the Specification Translator to resolve some of the issues identified in the previous chapter. This tool is capable of translating specifications while taking into account the semantics of the specification languages. Currently it supports the specification languages used by Krakatoa, OpenJML and VerCors.
As a result, we are now able to share specifications between these tools. This allows us to reuse case studies, API specifications, and translate output from specification inference tools thereby enhancing their impact.
To conclude, this thesis aims to reduce the specification bottleneck for deductive verification. It does this by enhancing our theoretical understanding of the different types of specifications. Moreover, it provides a tool that allows us to reuse contracts for verification, thereby also providing a practical way to reduce the specification bottleneck. By reducing the specification bottleneck, we come a step closer to using deductive verification in practice. Thereby improving the reliability of software in our daily lives.
