Minimal structures for program analysis and verification
The reliability of software systems is a key societal concern. Because software should provide versatile functionalities in a myriad of contexts, the conception, design, and validation of programs remains a complex task.
Techniques for (automated) software verification are very important. Nowadays, it is widely accepted that formal methods can play a decisive role towards reliable software. Formal methods refer to a broad set of mathematical techniques that allow us to precisely describe software and its intended properties. Relying on mathematical foundations, these techniques provide strong guarantees for correctness.
The practical adoption of formal methods, however, still lags behind. There are two key challenges: (i) an increased learning curve for developers, and (ii) the associated analysis techniques come with their own implementation complexity. There is both practical and theoretical interest in rigorously studying simpler, or even minimal, formulations of the mathematical structures that underpin formal methods.
In his thesis, Alan Arslanagic focussed on two such structures: typestates and session types. They both specify software properties that vary over time (i.e., temporal properties). Arslanagic provides evidence that simpler formulations of these structures can lead to both practical and theoretical benefits. On the practical side, Arslanagic's formulations enable considerable usability and performance improvements and streamlined embedding into mainstream programming languages. On the theoretical side, he establishes a precise relationship between his formulations and the original ones, fully justifying the benefits of adopting simplerformulations.