Abstract
This thesis studies the field of program verification and deductive verification.
Important topics that can help to increase the reliability of software.
The first part of this thesis focuses on the tools that are currently available for program verification. There are many different tools, and it can be difficult to find the right tool for you. We provide a megamodel to distinguish these tools. Moreover, we set up a data set containing many program verification tools that have been categorised according to this megamodel. This provides a concrete point for users where they can explore what kind of program verification tools exist and might be right for them. We also explore the trends that we can see in the different levels of the megamodel.
Next, we focus on the usability of deductive verification. Deductive verifiers require the user to annotate programs with specifications, which limits its scalability in practice. Therefore, we investigate what types of specifications are used in deductive verification of Java programs, and how often these different types occur. This has been done by providing a taxonomy that categorises the specifications. Moreover, a data set has been set up which contains specifications used by several deductive verifiers. This data is statistically analysed to infer how often different types of specifications are expected to occur.
Then, we provide an overview of specification inference tools that can be used to generate specifications for Java programs. We use the taxonomy presented earlier to estimate the impact of these specification inference tools. Based on this, we identify gaps in the current state of the art.
Finally, we address the problem of specification reuse in deductive verification by providing a tool that can automatically translate specifications between various specification languages.
This allows us to reuse case studies, API specifications, and translate output from specification inference tools thereby enhancing their impact.
Important topics that can help to increase the reliability of software.
The first part of this thesis focuses on the tools that are currently available for program verification. There are many different tools, and it can be difficult to find the right tool for you. We provide a megamodel to distinguish these tools. Moreover, we set up a data set containing many program verification tools that have been categorised according to this megamodel. This provides a concrete point for users where they can explore what kind of program verification tools exist and might be right for them. We also explore the trends that we can see in the different levels of the megamodel.
Next, we focus on the usability of deductive verification. Deductive verifiers require the user to annotate programs with specifications, which limits its scalability in practice. Therefore, we investigate what types of specifications are used in deductive verification of Java programs, and how often these different types occur. This has been done by providing a taxonomy that categorises the specifications. Moreover, a data set has been set up which contains specifications used by several deductive verifiers. This data is statistically analysed to infer how often different types of specifications are expected to occur.
Then, we provide an overview of specification inference tools that can be used to generate specifications for Java programs. We use the taxonomy presented earlier to estimate the impact of these specification inference tools. Based on this, we identify gaps in the current state of the art.
Finally, we address the problem of specification reuse in deductive verification by providing a tool that can automatically translate specifications between various specification languages.
This allows us to reuse case studies, API specifications, and translate output from specification inference tools thereby enhancing their impact.
Original language | English |
---|---|
Qualification | Doctor of Philosophy |
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 17 Oct 2023 |
Place of Publication | Enschede |
Publisher | |
Print ISBNs | 978-90-365-5845-7 |
Electronic ISBNs | 978-90-365-5846-4 |
DOIs | |
Publication status | Published - 17 Oct 2023 |