Solving the VerifyThis 2012 challenges with VeriFast | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

Solving the VerifyThis 2012 challenges with VeriFast

  • VerifyThis 2012
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We describe our experience solving the VerifyThis 2012 challenges with our program verification tool VeriFast, including detailed explanations of our solutions. We also describe some alternative solutions that we developed after the competition. VeriFast is a modular verifier that takes Java or C source code annotated with function/method specifications written in a variant of separation logic, and verifies that the code complies with the annotations through symbolic execution.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10

Similar content being viewed by others

Notes

  1. The only differences with the actual submitted code are (1) that this version uses an improved notation for array permissions which was introduced in the December 2012 release of VeriFast, and (2) that we removed some ghost statements that turned out to be superfluous.

  2. The only differences with the actual submitted code are (1) that this version is written in C instead of Java, (2) that it uses the improved notation for array permissions as before, and (3) that quantifiers are expressed via \({\mathtt {forall}}\) instead of \(\mathtt {forall\_nth}\).

References

  1. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004)

    Book  Google Scholar 

  2. Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. POPL (2005)

  3. de Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. In: Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer, Berlin (2008)

  4. Filliâtre, J.-C., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: Klebanov, V., Grebing, S. (eds.), COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems. Manchester, UK, June 2012. EasyChair (2012)

  5. Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12(10) (1969)

  6. Huisman, M., Klebanov, V., Monahan, R.: The VerifyThis 2012 website. http://fm2012.verifythis.org/ (2012)

  7. Jacobs, B., Smans, J., Piessens, F.: The VeriFast website. http://distrinet.cs.kuleuven.be/software/VeriFast/ (2013)

  8. Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Rustan, K., Leino, M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Weiß, B.: The 1st Verified Software Competition: Experience report. In: Butler, M., Schulte W. (eds) Proceedings, 17th International Symposium on Formal Methods (FM), vol. 6664 of LNCS. Springer, Berlin (2011)

  9. Nipkow, Tobias: Interactive proof: Introduction to Isabelle/HOL. In: Grumberg, O., Nipkow, T., Hauptmann, B. (eds.) Software Safety and Security, pp. 254–285. IOS Press, Amsterdam (2012)

    Google Scholar 

  10. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. CSL (2001)

  11. Parkinson, M., Bierman, G.: Separation logic and abstraction. POPL (2005)

  12. Philippaerts, P., Mühlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: industrial case studies. Sci. Comput. Progr (2013)

  13. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. LICS (2002)

  14. Tuerk, T.: Local reasoning about while-loops. In: VSTTE Theory Workshop (2010)

Download references

Acknowledgments

This research is partially funded by the Research Fund KU Leuven, and by the EU FP7 project NESSoS. With the financial support from the Prevention of and Fight against Crime Programme of the European Union (B-CCENTRE). Jan Smans is a postdoctoral fellow of the Fund for Scientific Research Flanders (FWO). We acknowledge support from Microsoft Research Cambridge as part of the Verified Software Initiative.

Author information

Authors and Affiliations

  1. iMinds-DistriNet, KU Leuven, 3001 , Leuven, Belgium

    Bart Jacobs, Jan Smans & Frank Piessens

Authors
  1. Bart Jacobs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jan Smans
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frank Piessens
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bart Jacobs.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Jacobs, B., Smans, J. & Piessens, F. Solving the VerifyThis 2012 challenges with VeriFast. Int J Softw Tools Technol Transfer 17, 659–676 (2015). https://doi.org/10.1007/s10009-014-0310-9

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-014-0310-9

Keywords

Search

Navigation