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.

References in zbMATH (referenced in 28 articles )

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

1 2 next

  1. Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben: Model checking for symbolic-heap separation logic with inductive predicates (2016)
  2. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  3. Duan, Zhenhua; Bu, Kangkang; Tian, Cong; Zhang, Nan: Model checking MSVL programs based on dynamic symbolic execution (2015)
  4. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  5. Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
  6. Charlton, Nathaniel; Reus, Bernhard: Specification patterns for reasoning about recursion through the store (2013)
  7. Enea, Constantin; Saveluc, Vlad; Sighireanu, Mihaela: Compositional invariant checking for overlaid and nested linked lists (2013)
  8. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  9. Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard: Crowfoot: a verifier for higher-order store programs (2012)
  10. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  11. Leino, K.Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  12. Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok: Two for the price of one: lifting separation logic assertions (2012)
  13. Chapman, Roderick; Botcazou, Eric; Wallenburg, Angela: SPARKSkein: a formal and fast reference implementation of Skein (2011) ioport
  14. Charlton, Nathaniel; Reus, Bernhard: Specification patterns and proofs for recursion through the store (2011)
  15. Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James: Tractable reasoning in a fragment of separation logic (2011)
  16. Crespo, Juan Manuel; Kunz, César: A machine-checked framework for relational separation logic (2011)
  17. Fähndrich, Manuel; Logozzo, Francesco: Static contract checking with abstract interpretation (2011)
  18. Jacobs, Bart; Smans, Jan; Philippaerts, Pieter; Vogels, Frédéric; Penninckx, Willem; Piessens, Frank: Verifast: A powerful, sound, predictable, fast verifier for C and Java (2011) ioport
  19. Le Goues, Claire; Leino, K.Rustan M.; Moskal, Michał: The Boogie verification debugger (tool paper) (2011) ioport
  20. Tschannen, Julian; Furia, Carlo A.; Nordio, Martin; Meyer, Bertrand: Usable verification of object-oriented programs by combining static and dynamic techniques (2011) ioport

1 2 next