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.


References in zbMATH (referenced in 52 articles )

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

1 2 3 next

  1. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  2. Duck, Gregory J.; Jaffar, Joxan; Yap, Roland H. C.: Shape neutral analysis of graph-based data-structures (2018)
  3. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  4. Charguéraud, Arthur; Pottier, François: Temporary Read-only permissions for separation logic (2017)
  5. Demri, Stéphane; Galmiche, Didier; Larchey-Wendling, Dominique; Méry, Daniel: Separation logic with one quantified variable (2017)
  6. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: \textscCaper- automatic verification for fine-grained concurrency (2017)
  7. Enea, Constantin; Lengál, Ondřej; Sighireanu, Mihaela; Vojnar, Tomáš: Compositional entailment checking for a fragment of separation logic (2017)
  8. Hirsch, Robin; McLean, Brett: Disjoint-union partial algebras (2017)
  9. Hóu, Zhé; Sanán, David; Tiu, Alwen; Liu, Yang: Proof tactics for assertions in separation logic (2017)
  10. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  11. Roşu, Grigore: Matching logic (2017)
  12. Faisal Al Ameen, Mahmudul; Tatsuta, Makoto: Completeness for recursive procedures in separation logic (2016)
  13. Hóu, Zhé; Tiu, Alwen: Completeness for a first-order abstract separation logic (2016)
  14. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)
  15. Maclean, Ewen; Ireland, Andrew; Grov, Gudmund: Proof automation for functional correctness in separation logic (2016)
  16. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  17. Demri, Stéphane; Deters, Morgan: Separation logics and modalities: a survey (2015)
  18. Heinen, Jonathan; Jansen, Christina; Katoen, Joost-Pieter; Noll, Thomas: Juggrnaut: using graph grammars for abstracting unbounded heap structures (2015)
  19. Hóu, Zhé; Goré, Rajeev; Tiu, Alwen: Automated theorem proving for assertions in separation logic with all connectives (2015)
  20. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)

1 2 3 next