Abstract
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 this thesis, we focus on two such structures: typestates and session types. They both specify software properties that vary over time (i.e., temporal properties). We provide evidence that simpler formulations of these structures can lead to both practical and theoretical benefits. On the practical side, our formulations enable considerable usability and performance improvements and streamlined embedding into mainstream programming languages. On the theoretical side, we establish a precise relationship between our formulations and the original ones, fully justifying the benefits of adopting simpler
formulations.
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 this thesis, we focus on two such structures: typestates and session types. They both specify software properties that vary over time (i.e., temporal properties). We provide evidence that simpler formulations of these structures can lead to both practical and theoretical benefits. On the practical side, our formulations enable considerable usability and performance improvements and streamlined embedding into mainstream programming languages. On the theoretical side, we establish a precise relationship between our formulations and the original ones, fully justifying the benefits of adopting simpler
formulations.
| Original language | English |
|---|---|
| Qualification | Doctor of Philosophy |
| Awarding Institution |
|
| Supervisors/Advisors |
|
| Award date | 12-Sept-2023 |
| Place of Publication | [Groningen] |
| Publisher | |
| DOIs | |
| Publication status | Published - 2023 |