Deductive verification is a program verification technique where the user specifies how the program should behave. Tools then check whether the program adheres to the specification. Writing these specifications tends to take a lot of time and expertise. This limits the application of deductive verifiers in practice. This problem is sometimes called the “specification bottleneck”.

In this research we have a detailed look at the type of specifications that are required to verify a program with deductive verifiers. We made a taxonomy that distinguishes the different types of specifications that are used. We also set up a data set consisting of programs that have been verified and statistically analysed how often each type of specification is expected to occur. This data sheds light on which annotations in the deductive verification process need the most automation, simplification, and should be the focus of education.

Useful links

• Paper: Sophie Lathouwers and Marieke Huisman. 2022. Formal specifications investigated: a classification and analysis of annotations for deductive verifiers. In Proceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE ‘22). Association for Computing Machinery, New York, NY, USA, 69–79. https://doi.org/10.1145/3524482.3527652
• Artefact: https://doi.org/10.4121/16545714