The VeriFast Program Verifier
The work
| Authors | Bart Jacobs; Frank Piessens |
|---|---|
| Editors | |
| Type | techreport |
| Year | 2008 |
| Citekey | jacobs2008verifast |
Where it appeared
| Publisher | Katholieke Universiteit Leuven, Department of Computer Science |
|---|---|
| Number in series | CW 520 |
| School | Katholieke Universiteit Leuven, Department of Computer Science |
Access
| Landing page | https://www.cs.kuleuven.be/publicaties/rapporten/cw/CW520.pdf |
|---|
From bibtex.
Abstract
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.
A copy is held
pdf, 184.8 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-10-22 23:46 UTC |
| Approved by | a person 2026-10-23 07:51 UTC |
Filed under
Cite it as
@techreport{jacobs2008verifast,
title = {The VeriFast Program Verifier},
author = {Bart Jacobs and Frank Piessens},
year = {2008},
publisher = {Katholieke Universiteit Leuven, Department of Computer Science},
school = {Katholieke Universiteit Leuven, Department of Computer Science},
}
This record lives at https://refs.drheap.org/jacobs2008verifast/ and will keep doing so.