Smallfoot: Modular automatic assertion checking with separation logic. Separation logic is a program logic for reasoning about programs that manipulate pointer data structures. We describe Smallfoot, a tool for checking certain lightweight separation logic specifications. The assertions describe the shapes of data structures rather than their detailed contents, and this allows reasoning to be fully automatic. The presentation in the paper is tutorial in style. We illustrate what the tool can do via examples which are oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what a procedure does not change); embracement of “dirty” features such as memory disposal and address arithmetic; information hiding in the presence of pointers; and modular reasoning about concurrent programs.

References in zbMATH (referenced in 30 articles )

Showing results 1 to 20 of 30.
Sorted by year (citations)

1 2 next

  1. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  2. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: Caper - automatic verification for fine-grained concurrency (2017)
  3. Hirsch, Robin; McLean, Brett: Disjoint-union partial algebras (2017)
  4. Faisal Al Ameen, Mahmudul; Tatsuta, Makoto: Completeness for recursive procedures in separation logic (2016)
  5. Maclean, Ewen; Ireland, Andrew; Grov, Gudmund: Proof automation for functional correctness in separation logic (2016)
  6. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  7. Heinen, Jonathan; Jansen, Christina; Katoen, Joost-Pieter; Noll, Thomas: Juggrnaut: using graph grammars for abstracting unbounded heap structures (2015)
  8. Hóu, Zhé; Goré, Rajeev; Tiu, Alwen: Automated theorem proving for assertions in separation logic with all connectives (2015)
  9. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  10. Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
  11. Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
  12. Lee, Wonyeol; Park, Sungwoo: A proof system for separation logic with magic wand (2014)
  13. Charlton, Nathaniel; Reus, Bernhard: Specification patterns for reasoning about recursion through the store (2013)
  14. Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)
  15. Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao: Automated verification of shape, size and bag properties via user-defined predicates in separation logic (2012)
  16. Stewart, Gordon; Beringer, Lennart; Appel, Andrew W.: Verified heap theorem prover by paramodulation (2012)
  17. Appel, Andrew W.: VeriSmall: verified Smallfoot shape analysis (2011) ioport
  18. Calcagno, Cristiano; Distefano, Dino; O’Hearn, Peter W.; Yang, Hongseok: Compositional shape analysis by means of bi-abduction (2011)
  19. Charlton, Nathaniel; Reus, Bernhard: Specification patterns and proofs for recursion through the store (2011)
  20. Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James: Tractable reasoning in a fragment of separation logic (2011)

1 2 next