Smallfoot swMATH ID: 9787 Software Authors: Berdine, J., Calcagno, C., O’Hearn, P.W. Description: 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. Homepage: http://link.springer.com/chapter/10.1007/11804192_6 Related Software: jStar; VeriFast; z3; Coq; HIP; SLAyer; Spec#; Isabelle; Slide; Boogie; Why3; Infer; Viper; JML; KRAKATOA; Crowfoot; VerCors; Dafny; Caduceus; Eiffel Cited in: 51 Publications all top 5 Cited by 116 Authors 4 Charlton, Nathaniel 4 Demri, Stéphane P. 4 Reus, Bernhard 3 Calcagno, Cristiano 3 Hou, Zhe 3 Tiu, Alwen Fernanto 2 Brochenin, Rémi 2 Chin, Wei-Ngan 2 David, Cristina 2 Galmiche, Didier 2 Gardner, Philippa Anne 2 Gast, Holger 2 Horsfall, Ben 2 Huisman, Marieke 2 Jansen, Christina 2 Lozes, Etienne 2 Méry, Daniel 2 Müller, Peter 2 Nguyen, Huu Hai 2 Noll, Thomas 2 O’Hearn, Peter W. 2 Qin, Shengchao 1 Amighi, Afshin 1 Andersen, Kristoffer Just Arndal 1 Appel, Andrew W. 1 Bansal, Kshitij 1 Bao, Yuyan 1 Beringer, Lennart 1 Birkedal, Lars 1 Bjørner, Nikolaj S. 1 Blom, Stefan 1 Charguéraud, Arthur 1 Chen, Yiyun 1 Chlipala, Adam J. 1 Cook, Byron 1 da Rocha Pinto, Pedro 1 Darabi, Saeed 1 de Moura, Leonardo 1 Deters, Morgan 1 Dinsdale-Young, Thomas 1 Distefano, Dino 1 Dong, Yuan 1 Duck, Gregory J. 1 Emmi, Michael 1 Enea, Constantin 1 Ernst, Gidon 1 Faisal Al Ameen, Mahmudul 1 Feng, Xinyu 1 Goré, Rajeev Prabhakar 1 Grov, Gudmund 1 Guo, Yu 1 Haase, Christoph 1 Heinen, Jonathan 1 Hirsch, Robin 1 Hobor, Aquinas 1 Hurlin, Clément 1 Ireland, Andrew 1 Jacobs, Bart 1 Jaffar, Joxan 1 Jeannet, Bertrand 1 Jhala, Ranjit 1 Katelaan, Jens 1 Katoen, Joost-Pieter 1 Kohler, Eddie 1 Kröning, Daniel 1 Kugler, Hillel 1 Larchey-Wendling, Dominique 1 Leavens, Gary T. 1 Lee, Wonyeol 1 Leino, K. Rustan M. 1 Lengál, Ondřej 1 Leow, Wei Xiang 1 Li, Zhaopeng 1 Liu, Yang 1 Loginov, Alexey 1 Maclean, Ewen 1 Madlener, Ken 1 Majumdar, Rupak 1 Malecha, Gregory 1 Matheja, Christoph 1 McCreight, Andrew 1 Mclean, Brett 1 Mohan, Anshuman 1 Morrisett, Greg 1 Mostowski, Wojciech I. 1 Ouaknine, Joel O. 1 Park, Sungwoo 1 Parkinson, Matthew J. 1 Piessens, Frank 1 Pottier, François 1 Raza, Mohammad 1 Reps, Thomas W. 1 Roşu, Grigore 1 Safari, Mohsen 1 Sagiv, Mooly 1 Sanán, David 1 Schwerhoff, Malte 1 Shao, Zhong 1 Shinnar, Avraham 1 Sighireanu, Mihaela ...and 16 more Authors all top 5 Cited in 15 Serials 3 Formal Methods in System Design 3 Logical Methods in Computer Science 2 Theoretical Computer Science 2 Journal of Automated Reasoning 2 Journal of Logic and Computation 1 Science of Computer Programming 1 Annals of Pure and Applied Logic 1 Journal of Computer Science and Technology 1 Information and Computation 1 Formal Aspects of Computing 1 Journal of Applied Non-Classical Logics 1 Theory of Computing Systems 1 Journal of the ACM 1 Theory and Practice of Logic Programming 1 Texts in Theoretical Computer Science. An EATCS Series Cited in 3 Fields 48 Computer science (68-XX) 32 Mathematical logic and foundations (03-XX) 1 General algebraic systems (08-XX) Citations by Year