Smallfoot
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.
Keywords for this software
References in zbMATH (referenced in 27 articles )
Showing results 1 to 20 of 27.
Sorted by year (- Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
- Faisal Al Ameen, Mahmudul; Tatsuta, Makoto: Completeness for recursive procedures in separation logic (2016)
- Maclean, Ewen; Ireland, Andrew; Grov, Gudmund: Proof automation for functional correctness in separation logic (2016)
- Heinen, Jonathan; Jansen, Christina; Katoen, Joost-Pieter; Noll, Thomas: Juggrnaut: using graph grammars for abstracting unbounded heap structures (2015)
- Hóu, Zhé; Goré, Rajeev; Tiu, Alwen: Automated theorem proving for assertions in separation logic with all connectives (2015)
- Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
- Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
- Amighi, Afshin; Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Mostowski, Wojciech; Zaharieva-Stojanovski, Marina: Verification of concurrent systems with VerCors (2014)
- Lee, Wonyeol; Park, Sungwoo: A proof system for separation logic with magic wand (2014)
- Charlton, Nathaniel; Reus, Bernhard: Specification patterns for reasoning about recursion through the store (2013)
- Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)
- 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)
- Stewart, Gordon; Beringer, Lennart; Appel, Andrew W.: Verified heap theorem prover by paramodulation (2012)
- Appel, Andrew W.: VeriSmall: verified Smallfoot shape analysis (2011)
- Calcagno, Cristiano; Distefano, Dino; O’Hearn, Peter W.; Yang, Hongseok: Compositional shape analysis by means of bi-abduction (2011)
- Charlton, Nathaniel; Reus, Bernhard: Specification patterns and proofs for recursion through the store (2011)
- Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James: Tractable reasoning in a fragment of separation logic (2011)
- Galmiche, Didier; Méry, Daniel: Tableaux and resource graphs for separation logic (2010)
- Gast, Holger: Reasoning about memory layouts (2010)
- Brochenin, Rémi; Demri, Stéphane; Lozes, Etienne: Reasoning about sequences of memory states (2009)