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 24 articles )

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

1 2 next

  1. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  2. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  3. Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
  4. Charlton, Nathaniel; Reus, Bernhard: Specification patterns for reasoning about recursion through the store (2013)
  5. Enea, Constantin; Saveluc, Vlad; Sighireanu, Mihaela: Compositional invariant checking for overlaid and nested linked lists (2013)
  6. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  7. Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard: Crowfoot: a verifier for higher-order store programs (2012)
  8. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  9. Leino, K.Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  10. Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok: Two for the price of one: lifting separation logic assertions (2012)
  11. Chapman, Roderick; Botcazou, Eric; Wallenburg, Angela: SPARKSkein: A formal and fast reference implementation of Skein (2011)
  12. Charlton, Nathaniel; Reus, Bernhard: Specification patterns and proofs for recursion through the store (2011)
  13. Cook, Byron; Haase, Christoph; Ouaknine, Joël; Parkinson, Matthew; Worrell, James: Tractable reasoning in a fragment of separation logic (2011)
  14. Crespo, Juan Manuel; Kunz, César: A machine-checked framework for relational separation logic (2011)
  15. Fähndrich, Manuel; Logozzo, Francesco: Static contract checking with abstract interpretation (2011)
  16. Le Goues, Claire; Leino, K.Rustan M.; Moskal, Michał: The Boogie verification debugger (tool paper) (2011)
  17. Tschannen, Julian; Furia, Carlo A.; Nordio, Martin; Meyer, Bertrand: Usable verification of object-oriented programs by combining static and dynamic techniques (2011)
  18. Bubel, Richard; Hähnle, Reiner; Ji, Ran: Interleaving symbolic execution and partial evaluation (2010)
  19. Cherini, Renato; Rearte, Lucas; Blanco, Javier: A shape analysis for non-linear data structures (2010)
  20. Leino, K.Rustan M.: Dafny: an automatic program verifier for functional correctness (2010)

1 2 next