Document Open Access Logo

Lightweight Support for Magic Wands in an Automatic Verifier

Authors Malte Schwerhoff, Alexander J. Summers

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.614.pdf
  • Filesize: 0.64 MB
  • 25 pages

Document Identifiers

Author Details

Malte Schwerhoff
Alexander J. Summers

Cite As Get BibTex

Malte Schwerhoff and Alexander J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 614-638, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.ECOOP.2015.614

Abstract

Permission-based verification logics such as separation logic have led to the development of many practical verification tools over the last decade. Verifiers employ the separating conjunction A*B to elegantly handle aliasing problems, framing, race conditions, etc.

Introduced along with the separating conjunction, the magic wand connective, written A -* B, can describe hypothetical modifications of the current state, and provide guarantees about the results. Its formal semantics involves quantifying over states: as such, the connective is typically not supported in automatic verification tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, for example, for specifying loop invariants and partial data structures.

In this paper, we show how to integrate support for the magic wand into an automatic verifier, requiring low specification overhead from the tool user, due to a novel approach for choosing footprints for magic wand formulas automatically. We show how to extend this technique to interact elegantly with common specification features such as recursive predicates. Our solution is designed to be compatible with a variety of logics and underlying implementation techniques.

We have implemented our approach, and a prototype verifier is available to download, along with a collection of examples.

Subject Classification

Keywords
  • Magic Wand
  • Software Verification
  • Automatic Verifiers
  • Separation Logic
  • Implicit Dynamic Frames

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, pages 115-137, 2005. Google Scholar
  2. Stefan Blom and Marieke Huisman. Witnessing the elimination of magic wands. Technical Report TR-CTIT-13-22, University of Twente, November 2013. Google Scholar
  3. John Tang Boyland. Checking interference with fractional permissions. In SAS, 2003. Google Scholar
  4. John Tang Boyland. Semantics of fractional permissions with nesting. ACM Trans. Program. Lang. Syst., 32(6):22:1-22:33, August 2010. Google Scholar
  5. Rémi Brochenin, Stéphane Demri, and Etienne Lozes. On the almighty wand. Journal of Information and Computation, 211:106-137, February 2012. Google Scholar
  6. James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. Automated cyclic entailment proofs in separation logic. In CADE'11, pages 131-146, 2011. Google Scholar
  7. Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming, 77(9):1006-1036, 2012. Google Scholar
  8. Dino Distefano and Matthew J. Parkinson. jStar: towards practical verification for java. In OOPSLA, pages 213-226, 2008. Google Scholar
  9. Mike Dodds, Suresh Jagannathan, and Matthew J. Parkinson. Modular reasoning for deterministic parallelism. In POPL, pages 259-270, 2011. Google Scholar
  10. Christian Haack and Clément Hurlin. Resource usage protocols for iterators. Journal of Object Technology, 8:55-83, 2009. Google Scholar
  11. Stefan Heule, Ioannis T. Kassios, Peter Müller, and Alexander J. Summers. Verification condition generation for permission logics with abstract predicates and abstraction functions. In ECOOP, pages 451-476, 2013. Google Scholar
  12. Aquinas Hobor and Jules Villard. The ramifications of sharing in data structures. In POPL'13, pages 523-536. ACM, 2013. Google Scholar
  13. Zhe Hou, Ranald Clouston, Rajeev Goré, and Alwen Tiu. Proof search for propositional abstract separation logics via labelled sequents. In POPL, pages 465-476, 2014. Google Scholar
  14. Bart Jacobs and Frank Piessens. The VeriFast program verifier. Technical report, Katholieke Universiteit Leuven, August 2008. Google Scholar
  15. Jonas Braband Jensen, Lars Birkedal, and Peter Sestoft. Modular verification of linked lists with views via separation logic. Journal of Object Technology, 10:2:1-20, 2011. Google Scholar
  16. U. Juhasz, I. T. Kassios, P. Müller, M. Novacek, M. Schwerhoff, and A. J. Summers. Viper: A verification infrastructure for permission-based reasoning. Technical report, ETH Zurich, 2014. Google Scholar
  17. Neelakantan R. Krishnaswami. Reasoning about iterators with separation logic. In SVCBS, pages 83-86, New York, NY, USA, 2006. ACM. Google Scholar
  18. Oukseh Lee, Hongseok Yang, and Rasmus Petersen. Program analysis for overlaid data structures. In CAV, volume 6806 of LNCS, pages 592-608. Springer Berlin Heidelberg, 2011. Google Scholar
  19. Wonyeol Lee and Sungwoo Park. A proof system for separation logic with magic wand. In POPL, pages 477-490, 2014. Google Scholar
  20. K. Rustan M. Leino. This is Boogie 2. Available from http://research.microsoft.com/en-us/um/people/leino/papers.html.
  21. K. Rustan M. Leino and Peter Müller. A basis for verifying multi-threaded programs. In ESOP, pages 378-393, 2009. Google Scholar
  22. Toshiyuki Maeda, Haruki Sato, and Akinori Yonezawa. Extended alias type system using separating implication. In TLDI, pages 29-42. ACM, 2011. Google Scholar
  23. Huu Hai Nguyen and Wei-Ngan Chin. Enhancing program verification with lemmas. In CAV, volume 5123 of LNCS, pages 355-369. Springer Berlin Heidelberg, 2008. Google Scholar
  24. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, pages 1-19, London, UK, 2001. Springer-Verlag. Google Scholar
  25. M. Parkinson and G. Bierman. Separation logic and abstraction. In POPL, pages 247-258. ACM Press, 2005. Google Scholar
  26. M. J. Parkinson and A. J. Summers. The relationship between separation logic and implicit dynamic frames. In LMCS, 8(3:01):1-54, 2012. Google Scholar
  27. Ruzica Piskac, Thomas Wies, and Damien Zufferey. GRASShopper - complete heap verification with mixed specifications. In TACAS, pages 124-139. Springer, 2014. Google Scholar
  28. William S. Retert. Implementing Permission Analysis. PhD thesis, University of Wisconsin at Milwaukee, Milwaukee, WI, USA, 2009. Google Scholar
  29. Malte Schwerhoff and Alexander J. Summers. Implementation. Available from URL: https://www.pm.inf.ethz.ch/research/viper.html.
  30. Jan Smans. Specification and Automatic Verification of Frame Properties for Java-like Programs. PhD thesis, FWO-Vlaanderen, May 2009. Google Scholar
  31. Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In ECOOP, pages 148-172, 2009. Google Scholar
  32. Jan Smans, Bart Jacobs, and Frank Piessens. Heap-dependent expressions in separation logic. In FMOODS/FORTE, pages 170-185, 2010. Google Scholar
  33. Alexander J. Summers and Sophia Drossopoulou. A formal semantics for isorecursive and equirecursive state abstractions. In ECOOP, pages 129-153, 2013. Google Scholar
  34. Thomas Tuerk. Local reasoning about while-loops. In VSTTE, 2010. Google Scholar
  35. Hongseok Yang. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In SPACE, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact