Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010)
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)
VeriFast tutorial. http://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf
Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459–465. Springer, Heidelberg (2011)
Vogels, F., Jacobs, B., Piessens, F., Smans, J.: Annotation inference for separation logic based verifiers. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 319–333. Springer, Heidelberg (2011)
Mühlberg, J.T., White, D.H., Dodds, M., Lüttgen, G., Piessens, F.: Learning assertions to verify linked-list programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 37–52. Springer, Heidelberg (2015)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of BI-abduction. In: POPL (2009)
https://github.com/Mahmohsen/verifast/tree/Automated-Verifast
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)
Acknowledgments
This work was funded by the Flemish Research Fund through grant G.0058.13.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Mohsen, M., Jacobs, B. (2016). One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast. In: ter Beek, M., Gnesi, S., Knapp, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2016 2016. Lecture Notes in Computer Science(), vol 9933. Springer, Cham. https://doi.org/10.1007/978-3-319-45943-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-45943-1_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-45942-4
Online ISBN: 978-3-319-45943-1
eBook Packages: Computer ScienceComputer Science (R0)