Skip to content

VeriFast

Jump to bottom Edit New page
Bart Jacobs edited this page Oct 31, 2023 · 1 revision

VeriFast is a deductive program verifier for C, Java, C++, and Rust programs. The core features of VeriFast are:

  • Support of a large subset of the C language, including loops, recursion, integer types with overflows, floating point types, pointer arithmetic, structs, unions, ...
  • Flags control the precise C semantics: whether signed integer overflow is allowed (-fwrapv), whether arbitrary typecasts are allowed (-fno-strict-aliasing), whether arbitrary pointer arithmetic is allowed (i.e. whether pointer provenance is ignored), ...
  • Support of a large subset of the Java language, including loops, recursion, exceptions, integer types with overflows, floating point types, inheritance, static initialization, ...
  • Support of a core subset of C++, including all of the supported C features and most of the supported Java features, plus multiple inheritance, but templates support is under development
  • Under development: support for unsafe Rust code (purely unsafe code as well as soundness of safe abstractions built using unsafe code)
  • Modular specification/verification
  • Memory/heap modeling via separation logic
  • Program transformation to first-order via Symbolic Execution
  • Concurrency, including fine-grained concurrency, deadlock-freedom, and termination of busy waiting
  • Safety and liveness of I/O behavior

What inputs are supported?

C, Java, C++, Rust (under development), specifications in VeriFast's own separation logic-based annotation syntax.

For which programming languages has it support?

C (see supported grammar), Java (see supported grammar), C++, Rust (under development)

What properties can be verified?

For C, C++, and Rust, VeriFast verifies absence of undefined behavior (i.e. invalid memory accesses, data races, integer overflows (unless annotated as intentional using /*@ truncating @*/ and allowed by the chosen C semantics), etc.) as well as compliance with user-provided functional specifications and specifications for the APIs used. For Java, VeriFast verifies absence of array-index-out-of-bounds errors, null dereferences, integer overflows (unless annotated as intentional using /*@ truncating @*/), and data races, as well as compliance with user-provided functional specifications and specifications for the APIs used.

What are the tool’s main techniques for the supported (input, property) pairs?

VeriFast performs modular symbolic execution using a separation logic-based representation of memory. For this, it relies on user-provided preconditions, postconditions, loop invariants, data structure layout specifications in the form of separation logic predicates, and proof hints in the form of ghost commands for folding and unfolding predicates, invoking lemmas, etc. VeriFast performs limited proof search with no backtracking, to keep interactive performance predictable and fast.

What external tools are used? (e.g., compilers, SMT solvers)

VeriFast relies on an SMT solver for reasoning about data values. By default, it uses its built-in Redux solver (a partial re-implementation in OCaml of the venerable Simplify SMT solver), but it can also use Z3, and, via SMT-LIB, CVC4 and others.

What is the tool’s URL?

Example(s)

Example files are shipped with the tool, see here:

References

Add a custom footer

list of tools

list of challenges

Clone this wiki locally