VeriFast swMATH ID: 7705 Software Authors: Bart Jacobs; Jan Smans; Frank Piessens Description: The VeriFast program verifier. This note describes a separation-logic-based approach for the specification and verification of safety properties of pointer-manipulating imperative programs. The programmer may declare inductive datatypes and primitive recursive functions for specification. Verification proceeds by symbolic execution using an abstract representation of memory as a separation logic assertion. Folding or unfolding abstract predicate assertions is performed through explicit ghost statements. Lemma functions enable inductive proofs of memory representation equivalences and facts about the primitive recursive functions. An SMT solver is used to solve queries over data values; an algorithm is described that prevents non-termination of the SMT solver while enabling reduction of any ground term. Since no significant search is performed by either the verifier or the SMT solver, verification time is predictable and low. Homepage: http://people.cs.kuleuven.be/~bart.jacobs/verifast/ Related Software: Dafny; Boogie; z3; Coq; Why3; VCC; Spec#; jStar; Smallfoot; KRAKATOA; Viper; Frama-C; JML; Chalice; ESC/Java; CVC4; HIP; Isabelle/HOL; SLAyer; SIMPLIFY Cited in: 71 Documents all top 5 Cited by 160 Authors 6 Leino, K. Rustan M. 6 Müller, Peter 5 Jacobs, Bart 5 Summers, Alexander J. 4 Charlton, Nathaniel 4 Huisman, Marieke 4 Piessens, Frank 4 Reus, Bernhard 3 Appel, Andrew W. 3 Birkedal, Lars 2 Ahrendt, Wolfgang 2 Brotherston, James 2 Ernst, Gidon 2 Filliâtre, Jean-Christophe 2 Gorogiannis, Nikos 2 Horsfall, Ben 2 Leavens, Gary T. 2 Matheja, Christoph 2 Oortwijn, Wytse 2 Parkinson, Matthew J. 2 Polikarpova, Nadia 2 Rowe, Reuben N. S. 2 Sergey, Ilya 2 Sighireanu, Mihaela 2 Wang, Qinshi 2 Zuleger, Florian 1 Abbasi, Rosa 1 Amighi, Afshin 1 Andersen, Kristoffer Just Arndal 1 Arusoaie, Andrei 1 Bannister, Callum 1 Bao, Yuyan 1 Bengtson, Jesper 1 Beringer, Lennart 1 Blanco, Javier Oscar 1 Blom, Stefan 1 Bobot, François 1 Böhl, Florian 1 Bouillaguet, Quentin 1 Bu, Kangkang 1 Bubel, Richard 1 Chakraborty, Supratik 1 Chechik, Marsha 1 Cheng, Shu 1 Cherini, Renato 1 Chimento, Jesús Mauricio 1 Chin, Wei-Ngan 1 Cohen, Joshua M. 1 Cook, Byron 1 Costea, Andreea 1 Crespo, Juan Manuel 1 da Rocha Pinto, Pedro 1 Dailler, Sylvain 1 Darabi, Saeed 1 Dardinier, Thibault 1 Darulova, Eva 1 Demri, Stéphane P. 1 Dinsdale-Young, Thomas 1 Dongol, Brijesh 1 Drossopoulou, Sophia Chloe 1 D’Souza, Deepak 1 Duan, Zhenhua 1 Duck, Gregory J. 1 Enea, Constantin 1 Fähndrich, Manuel 1 Ferrara, Pietro 1 Ghezzi, Carlo 1 Gomes, Victor B. F. 1 Greiner, Simon 1 Groves, Lindsay J. 1 Gupta, Ashutosh 1 Gurov, Dilian 1 Haase, Christoph 1 Hähnle, Reiner 1 Hatcliff, John 1 Hauzar, David 1 He, Guanhua 1 Höfner, Peter 1 Hurlin, Clément 1 Illous, Hugo 1 Itzhaky, Shachar 1 Jaffar, Joxan 1 Jansen, Christina 1 Jensen, Jonas Braband 1 Ji, Ran 1 Joosten, Sebastiaan J. C. 1 Kanovich, Max Iosifovich 1 Katelaan, Jens 1 Klein, Gerwin 1 Krishna, Siddharth 1 Kuncak, Viktor 1 Kunz, César 1 Lemerre, Matthieu 1 Logozzo, Francesco 1 Lozes, Etienne 1 Lucanu, Dorel 1 Lugiez, Denis 1 Marché, Claude 1 Menghi, Claudio 1 Mostowski, Wojciech I. ...and 60 more Authors all top 5 Cited in 13 Serials 5 Formal Aspects of Computing 3 Journal of Automated Reasoning 3 Formal Methods in System Design 2 Logical Methods in Computer Science 2 Journal of Logical and Algebraic Methods in Programming 1 ACM Computing Surveys 1 Programming and Computer Software 1 Theoretical Computer Science 1 Journal of Symbolic Computation 1 Information and Computation 1 Annals of Mathematics and Artificial Intelligence 1 Theory and Practice of Logic Programming 1 ACM Transactions on Computational Logic Cited in 4 Fields 70 Computer science (68-XX) 30 Mathematical logic and foundations (03-XX) 1 Numerical analysis (65-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year