×

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: Boogie; Dafny; z3; Why3; jStar; Smallfoot; Coq; Spec#; VCC; KRAKATOA; Frama-C; ESC/Java; JML; Viper; HIP; CVC4; Isabelle/HOL; SLAyer; Caduceus; GitHub
Cited in: 61 Publications
all top 5

Cited by 138 Authors

6 Leino, K. Rustan M.
5 Jacobs, Bart
5 Müller, Peter
4 Charlton, Nathaniel
4 Piessens, Frank
4 Reus, Bernhard
3 Birkedal, Lars
3 Huisman, Marieke
3 Summers, Alexander J.
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 Parkinson, Matthew J.
2 Rowe, Reuben N. S.
2 Sighireanu, Mihaela
1 Abbasi, Rosa
1 Amighi, Afshin
1 Andersen, Kristoffer Just Arndal
1 Appel, Andrew W.
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 Chechik, Marsha
1 Cheng, Shu
1 Cherini, Renato
1 Chimento, Jesús Mauricio
1 Chin, Wei-Ngan
1 Cook, Byron
1 Crespo, Juan Manuel
1 da Rocha Pinto, Pedro
1 Dailler, Sylvain
1 Darabi, Saeed
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 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 Kanovich, Max Iosifovich
1 Katelaan, Jens
1 Klein, Gerwin
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 Matheja, Christoph
1 Menghi, Claudio
1 Mostowski, Wojciech I.
1 Moy, Yannick
1 Mutilin, V. S.
1 Noll, Thomas
1 Oortwijn, Wytse
1 Ouaknine, Joel O.
1 Pace, Gordon J.
1 Park, Jonghyun
1 Park, Sungwoo
1 Peleg, Hila
1 Penninckx, Willem
1 Pfähler, Jörg
1 Polikarpova, Nadia
1 Qin, Shengchao
...and 38 more Authors

Citations by Year