Advertisement

One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast

  • Mahmoud MohsenEmail author
  • Bart Jacobs
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)

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.

Keywords

Annotations inference Program verification Separation logic 

Notes

Acknowledgments

This work was funded by the Flemish Research Fund through grant G.0058.13.

References

  1. 1.
    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)CrossRefGoogle Scholar
  2. 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. 3.
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of BI-abduction. In: POPL (2009)Google Scholar
  9. 9.
  10. 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

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.iMinds-DistriNet, Department of Computer ScienceKatholieke Universiteit LeuvenLeuvenBelgium

Personalised recommendations