VeriFast

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

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

1 2 3 next

  1. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  2. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  3. Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
  4. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  5. Duck, Gregory J.; Jaffar, Joxan; Yap, Roland H. C.: Shape neutral analysis of graph-based data-structures (2018)
  6. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  7. Summers, Alexander J.; Müller, Peter: Automating deductive verification for weak-memory programs (2018)
  8. Zhan, Bohua: Efficient verification of imperative programs using auto2 (2018)
  9. Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (2017)
  10. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: \textscCaper- automatic verification for fine-grained concurrency (2017)
  11. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  12. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  13. Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben: Model checking for symbolic-heap separation logic with inductive predicates (2016)
  14. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  15. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  16. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  17. Dongol, Brijesh; Gomes, Victor B. F.; Struth, Georg: A program construction and verification tool for separation logic (2015)
  18. Duan, Zhenhua; Bu, Kangkang; Tian, Cong; Zhang, Nan: Model checking MSVL programs based on dynamic symbolic execution (2015)
  19. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  20. Penninckx, Willem; Jacobs, Bart; Piessens, Frank: Sound, modular and compositional verification of the input/output behavior of programs (2015)

1 2 3 next