-
Notifications
You must be signed in to change notification settings - Fork 0
TriCera
TriCera [1] is an automated, open-source verification tool for C programs based on the concept of Constrained Horn Clauses (CHCs). In order to handle programs operating on heap, TriCera applies a novel theory of heaps [2], which enables the tool to hand off most of the required heap reasoning directly to the underlying CHC solver.
TriCera has a web interface with many examples.
A large subset of C (2011), extended with features that are useful for verification.
TriCera attempts to verify both implicit and explicit safety properties. Explicit properties are specified using assert and assume statements, or through ACSL-style contracts.
Implicitly, TriCera attempts to verify several memory-safety properties:
- all pointer-dereferences are checked for type safety,
- array accesses are checked to be within array bounds,
- (optionally) memory leaks are detected by ensuring all allocated memory on the heap is freed at program exit.
TriCera was recently extended [3] to support more expressive properties: sum, max, min and univeral / existential properties over arrays. This work is not on the main branch of TriCera yet; however support is planned.
TriCera translates (input, property) pairs into a set of Constrained Horn Clauses (CHCs). The output is then processed and solved by a CHC solver, such as Eldarica [4] or Spacer [5]. These CHC solvers, when they do not time out, return either sat / unsat accompanied by either a solution or a counterexample. A solution contains all program invariants, and a counterexample is a trace through the program leading to the violated property (i.e., assertion).
The CHCs produced by TriCera can be printed in the standard SMT-LIB format, or in Prolog.
TriCera supports automatic inference of function contracts and loop invariants, and can print these in ACSL syntax.
TriCera uses Eldarica as its main CHC solver by default; however, any CHC solver that supports the used theories can be used on the CHCs produced by TriCera.
https://github.com/uuverifiers/tricera
TriCera also has a web interface.
Many examples can be found on TriCera's web interface. Please note that the web interface currently does not display inferred contracts.
There are also slides available online about TriCera from [1].
- An example on contract inference.
- Another example on invariant inference.
While these examples can be explored online, the -acsl and -inv options (used to view inferred
ACSL annotations and invariants) are currently only available when running TriCera
from the command line. Support for these options is also planned to be added to
the web interface in a future update.
TriCera uses the currently non-standard theory of heaps [2] in its output CHCs. The external tool heap2array can be used to translate its output to a standard one that uses the theory of arrays. This allows other CHC solvers that do not support the theory of heaps to be used by TriCera.
[1] Zafer Esen, Philipp Rümmer, "Tricera: Verifying C Programs Using the Theory of Heaps", FMCAD 2022: 380-391.
[2] Zafer Esen, Philipp Rümmer, "An SMT-LIB Theory of Heaps", SMT 2022: 38-53
[3] Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer, "Automatic Program Instrumentation for Automatic Verification", CAV 2023: 281-304.
[4] Hossein Hojjat, Philipp Rümmer, "The ELDARICA Horn Solver", FMCAD 2018:1-7
[5] Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke, "Automatic Abstraction in SMT-Based Unbounded Software Model Checking", CAV 2013: 846-862