Closer to Reliable Software: Verifying functional behaviour of concurrent programs
Marina Zaharieva-Stojanovski
promotor: prof.dr. M. Huisman (UT)
Universiteit Twente
Date: 1 October, 2015
Thesis: PDF
Summary
Static formal verification techniques are an effective method for verification of software. They exploit the advantages of formal methods to statically prove that the implementation of a program satisfies its formally written specification. This makes formal verification especially powerful: any execution of the program is guaranteed to behave correctly. Therefore, these techniques are especially attractive for safety-critical systems, where correctness of the code is a crucial requirement.
Applying formal techniques for verification of concurrent software is appealing. First, concurrent software today is omnipresent, but it is especially prone to errors. Second, finding errors in concurrent software using standard dynamic testing techniques is difficult, because of the non-deterministic behaviour of this software. Unfortunately, formal verification of concurrent software is hard and faces many challenges.
This thesis contributes with novel formal techniques for verification of multithreaded programs. We focus mainly on verification of functional properties, i.e., properties that describe the behaviour of the program. Concretely, we work with axiomatic reasoning and use permission-based separation logic as our basic program logic.
First, we propose a new modular technique for verification of class invariants in concurrent programs. This technique allows breaking of class invariants at certain safe places in the program. The technique is flexible and permissive, and thus, can be applied in a broad range of practical examples. This approach is formalised on a concurrent object-oriented language.
Second, we propose a new way of specifying and verifying functional behaviour of methods in the program. Our technique uses separation logic-based reasoning to build an abstraction of the program represented as a process algebra term; by reasoning about the abstract model, we prove properties about the original program. This approach allows very expressive and intuitive specifications. It is formalised for a concurrent object-oriented language, and integrated into our verification tool VerCors.
Third, we propose how by using history-based reasoning, one can reason about concurrent programs with guarded blocks. Our technique allows proving both functional and non-blocking properties about these programs. Moreover, we develop also a reverse future-based reasoning technique that allows verification of programs with non-terminating threads. We formalise this method on a simplified procedural language.
Permission-based separation logic is a well-established and powerful logic: it ties values of shared locations with permissions to these locations, which is an effective way to guarantee data race-freedom. However, it seems that this approach is not very convenient for modular verification of functional properties.
What is common for our techniques is that we use permission-based separation logic as a basic logic to ensure data race-freedom. However, we modify this logic and allow separation between values, i.e., functional properties, and permissions. It shows that this separation is useful and can significantly increase the number of properties that we can prove about concurrent programs.