VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java

The work

AuthorsBart Jacobs; Jan Smans; Pieter Philippaerts; Frédéric Vogels; Willem Penninckx; Frank Piessens
Editors
Typeinproceedings
Year2011
Citekeyjacobs2011verifast

Where it appeared

Published inNASA Formal Methods
PublisherSpringer
Pages41--55

Identifiers

DOI10.1007/978-3-642-20398-5_4
OpenAlexW1565541828

Access

Landing pagehttps://doi.org/10.1007/978-3-642-20398-5_4
Free full texthttps://lirias.kuleuven.be/handle/123456789/312066

Related

Distinct frommuller2016viper

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.

A copy is held

pdf, 184.5 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-12 14:58 UTC

Filed under

lncs nfm piessens the-copy-is-not-the-work verifying-real-java

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},
  publisher    = {Springer},
  pages        = {41--55},
  doi          = {10.1007/978-3-642-20398-5_4},
}

This record lives at https://refs.drheap.org/jacobs2011verifast/ and will keep doing so.