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 did a literature review to identify the various approaches that have been proposed to generate specifications/annotations for deductive verification. We specifically provide:

• A survey of tools that generate formal specifications for Java programs
• Analyse the impact of these tools on the overall specification writing process
• Provide practical recommendations for future inference tool development
• Provide a list of open research problems for specification inference.

Useful links

• Paper: Sophie Lathouwers and Marieke Huisman. 2024. Survey of Annotation Generators for Deductive Verifiers. In Journal of Systems and Software, Vol. 211 ,111972. https://doi.org/10.1016/j.jss.2024.111972
• Artefact: https://doi.org/10.4121/9c83933e-8406-4e49-ac4d-1f8bb55ed988