One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast
VeriFast is a sound modular formal verification tool for C and Java programs. Based on separation logic and using symbolic execution, VeriFast can verify not only memory safety of programs but also full functional correctness. Formal verification is a powerful way of analyzing code, but not yet widely used in practice. Source code has to be annotated with formal specification mostly in the form of function preconditions and postconditions. In this paper, we present Automated VeriFast which is a new extension or an automation layer that lies on top of VeriFast that, given a partially annotated program, offers to attempt to incrementally improve the annotations, e.g. by inferring a fix to the specification of a program fragment that fails to verify. Our thesis is that such small, interactive inference steps will have practical benefits over non-interactive specification inference approaches by allowing the user to guide the inference process and by being simpler and therefore more predictable and diagnosable.
KeywordsAnnotations inference Program verification Separation logic
This work was funded by the Flemish Research Fund through grant G.0058.13.
- 2.O’Hearn, P.W.: A primer on separation logic (and automatic program verification and analysis). Software Safety and Security; Tools for Analysis and Verification. NATO Science for Peace and Security Series, vol. 33, pp. 286–318 (2012)Google Scholar
- 3.VeriFast tutorial. http://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf
- 8.Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of BI-abduction. In: POPL (2009)Google Scholar
- 10.Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Heidelberg (2015)Google Scholar