VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
The work
| Title | VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java |
|---|---|
| Authors | Bart Jacobs; Jan Smans; Pieter Philippaerts; Frédéric Vogels; Willem Penninckx; Frank Piessens |
| Type | conference paper |
| Year | 2011 |
| Citekey | jacobs2011verifast |
Where it appeared
| Published in | NASA Formal Methods |
|---|---|
| Publisher | Springer |
| Pages | 41--55 |
Identifiers
| DOI | 10.1007/978-3-642-20398-5_4 |
|---|---|
| OpenAlex | W1565541828 |
Access
| Landing page | https://doi.org/10.1007/978-3-642-20398-5_4 |
|---|---|
| Free full text | https://lirias.kuleuven.be/handle/123456789/312066 |
Abstract
VeriFast is a prototype verification tool for single-threaded and multithreaded C and Java programs. In this paper, we first describe the basic symbolic execution approach in some formal detail. Then we zoom in on two technical aspects: the approach to permission accounting, including fractional permissions, precise predicates, and counting permis- sions; and the approach to lemma function termination in the presence of dynamically-bound lemma function calls. Finally, we describe three ongoing efforts: application to JavaCard programs, integration of shape analysis, and application to Linux device drivers.
Copy held
| Kind | PDF, 189.0 kB |
|---|---|
| Retrieved | 2026-08-10 |
| Held | local, for personal reference |
| Where it came from | https://people.cs.kuleuven.be/~bart.jacobs/nfm2011.pdf |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Record | reviewed by a person |
| Approved | 2026-08-12 |
Cite it as
@inproceedings{jacobs2011verifast,
title = {VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java},
author = {Bart Jacobs and Jan Smans and Pieter Philippaerts and Frédéric Vogels and Willem Penninckx and Frank Piessens},
year = {2011},
booktitle = {NASA Formal Methods},
pages = {41--55},
publisher = {Springer},
doi = {10.1007/978-3-642-20398-5_4},
url = {https://lirias.kuleuven.be/handle/123456789/312066},
}
This record lives at https://refs.drheap.org/jacobs2011verifast/ and will keep doing so.