Bridging the Implementation Gap: Advances in Model-Based Concurrent Program Verification
Bob Rubbens is a PhD student in the department Formal Methods and Tools. (Co)Promotors are prof.dr. M. Huisman and dr. P. van den Bos from the faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), University of Twente.
Software has become ubiquitous in both industry and elsewhere. Sadly, there are many examples of software bugs disrupting daily life at a large scale, such as the 2014 Heartbleed vulnerability, or the global Crowdstrike outage in 2024. Therefore, ensuring correctness of these software systems is crucial.
This is, however, hard. In a single-threaded setting, memory safety and functional correctness are difficult to verify. In a concurrent software environment, robust software design becomes even more challenging. Here, execution is interleaved between threads, causing some bugs to only be triggered in specific interleavings. This makes correct software much more difficult to write.
One way of ensuring correctness of concurrent software is through formal methods. Formal methods can check if a program follows a mathematical specification. Automated tools that implement these techniques create an opportunity for users to prove correctness of their software at unprecedented scale. This thesis focuses on the auto-active deductive verifier VerCors, which verifies concurrent programs with contracts for memory safety and functional correctness.
Even though there have been successful applications of formal methods to industrial systems, uptake is still limited. We found this is partly because of a gap between the mental models of engineers and the abstractions offered by formal methods. We improve the situation by combining, and extending capabilities of, formal methods with different workflows and levels of abstraction. These hybrid formal methods have the potential to narrow the gap between practical software development and verification with formal methods. We explore this theme in three parts.
The first part of this thesis investigates the possible reasons for the lack of adoption of one particular formal method: auto-active deductive verification. We apply the VerCors deductive verifier to an industrial code base of the Technolution company, finding two bugs. We conclude tool support still needs to be further improved, and that it is hard to connect mental models of developers to the abstraction level required for verification annotations.
In the second part of the thesis, we try to narrow the gap between mental models and formal methods by combining two verification tools: VerCors and the component-based software development framework JavaBIP. The key feature of JavaBIP is that it separates the implementation of components in Java from the interaction between components. We call this combination Verified JavaBIP, which verifies implementations of JavaBIP models for memory safety and functional correctness. We implement support for Verified JavaBIP in VerCors, and also implement run-time verification support in JavaBIP. We illustrate Verified JavaBIP on the VerifyThis Long Term Verification Challenge.
In the third part of this thesis, we consider choreographies and deductive verification. Choreographies are a constrained language for describing protocols and distributed systems. In choreographies, messages are always well-typed, and endpoints never have to wait infinitely for messages. Choreographies also support code generation. To verify choreographies, VeyMont was introduced, allowing verification of all endpoints in one combined context. In this thesis, we make VeyMont more broadly applicable by extending it with shared memory and parameterization.
VeyMont initially did not support shared memory. This limited expressiveness of the choreographies, and made it impossible to use shared ghost state to prove correctness. We enable use of shared memory by adding stratified permissions to VeyMont, which is a new type of annotation that assigns memory annotations to endpoints. VeyMont also uses stratified permissions to preserve verification annotations during code generation, making generated code verifiable with VerCors, increasing robustness and maintainability. We verify a Tic-Tac-Toe choreography with three levels of optimization, demonstrating a trade-off between the volume of annotations required to verify the choreography and its run-time performance.
We also extend VeyMont choreographies with parameterization. Before, choreographies required the user to specify the number of endpoints upfront. This made it difficult to express distributed systems in VeyMont that naturally scale. We extend VeyMont to support choreographies with a parameterized number of endpoints. We impose modest restrictions on the syntax of choreographies to retain automation, and illustrate the extension by verifying a distributed summation choreography. This shows that despite the limitations imposed, the proposed support is sufficient to verify interesting choreographies.
To conclude, this thesis investigates the gap between formal methods and software engineering in industry. We do this by using a deductive verifier in an industrial setting, and determining what is missing in the state of the art. Moreover, we combine formal methods with different workflows and abstractions, as well as extend such hybrid formal methods, to further narrow the gap between formal methods and software design. This brings formal methods closer to industry, and hence will improve the reliability of software systems in the long term.
