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

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

1 2 3 4 next

  1. Safari, Mohsen; Huisman, Marieke: Formal verification of parallel prefix sum and stream compaction algorithms in CUDA (2022)
  2. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  3. Beringer, Lennart; Appel, Andrew W.: Abstraction and subsumption in modular verification of C programs (2021)
  4. Filliâtre, Jean-Christophe: Simpler proofs with decentralized invariants (2021)
  5. Illous, Hugo; Lemerre, Matthieu; Rival, Xavier: A relational shape abstract domain (2021)
  6. Rumreich, Laine; Sivilotti, Paolo A. G.: Formal verification of a Java component using the RESOLVE framework (2021)
  7. Oortwijn, Wytse; Gurov, Dilian; Huisman, Marieke: Practical abstractions for automated verification of shared-memory concurrency (2020)
  8. Vasilyev, A. A.; Mutilin, V. S.: Predicate extension of symbolic memory graphs for the analysis of memory safety correctness (2020)
  9. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  10. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  11. Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
  12. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  13. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  14. Demri, Stéphane; Lozes, Etienne; Lugiez, Denis: On symbolic heaps modulo permission theories (2018)
  15. Duck, Gregory J.; Jaffar, Joxan; Yap, Roland H. C.: Shape neutral analysis of graph-based data-structures (2018)
  16. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  17. Summers, Alexander J.; Müller, Peter: Automating deductive verification for weak-memory programs (2018)
  18. Zhan, Bohua: Efficient verification of imperative programs using auto2 (2018)
  19. 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)
  20. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: \textscCaper-- automatic verification for fine-grained concurrency (2017)

1 2 3 4 next