VeriSmall swMATH ID: 9788 Software Authors: Appel, Andrew W. Description: VeriSmall: verified smallfoot shape analysis. We have implemented a version of the Smallfoot shape analyzer, calling upon a paramodulation-based heap theorem prover. Our implementation is done in Coq and is extractable to an efficient ML program. The program is verified correct in Coq with respect to our Separation Logic for C minor; this in turn is proved correct in Coq w.r.t. Leroy’s operational semantics for C minor. Thus when our VeriSmall static analyzer claims some shape property of a program, an end-to-end machine-checked proof guarantees that the assembly language of the compiled program will actually have that property. Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-25379-9_18 Related Software: Coq; Charge!; Smallfoot; SLAyer; VeriFast; jStar; VCC; HOL; Isabelle/HOL; Dafny; Infer; seL4; HIP; Toolchain; C-to-Isabelle; CompCert; Frama-C; Gallina; VeriStar; Mechanized Semantic Library Cited in: 5 Publications all top 5 Cited by 12 Authors 2 Appel, Andrew W. 1 Bannister, Callum 1 Beringer, Lennart 1 Dodds, Josiah 1 Gherghina, Cristian 1 Hobor, Aquinas 1 Höfner, Peter 1 Jacobs, Bart 1 Klein, Gerwin 1 Piessens, Frank 1 Stewart, Gordon 1 Vogels, Frédéric Cited in 1 Serial 2 Logical Methods in Computer Science Cited in 2 Fields 5 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year