By Marieke Huisman
Software is everywhere. Failures in it can have enormous impact. All software have errors. Verifying software should become part of software development. It would be great if while developing verification already pops up, similar to current code completion and warnings; for example giving counter examples. This automatic feedback requires a lot of new research. Similar, we would like to enlarge the class of properties we can verify. Specifying program behaviour stems already from the 60’s, such as the Hoare triples with corresponding logic: {P} S {Q}, as I learned programming in Eindhoven with Dijkstra’s approach. For sequential problems, automated provers are becoming better and better. Concurrent programs however are a complete different story. Think of several threads writing and reading to shared memory. As soon as the number of threads increases, we cannot create a mental model of it anymore. A good example is the Therac-25. Another problem in concurrent software is its specification: other threads may threat postconditions. Separation Logic is one way to address this problem. Separation logic is an extension of Hoare Logic for handling memory with pointers.
Vercors is a tool for automated verification of concurrent software, which they applied on several languages with different concurrency paradigms, such as Java and OpenCL. Vercors uses Viper in the backend for verification. They use abstract histories to look at global behaviour, and merge local behaviour of threads (SEFM 2015, VSTTE 2017).
A counter example 🙂
In the near future, they want to look into different classes, and generating annotations automatically. However, one question that remains for me: how to specify the pre and post conditions? How do we train developers in this? Dijkstra programming is now considered old-fashioned…