uuverifiers / tricera

TriCera: a model checker for C programs
BSD 3-Clause "New" or "Revised" License
18 stars 13 forks source link

Summary

TriCera is a model checker for C programs, that is being developed and maintained by Uppsala University. TriCera accepts programs in a C-like language, and currently supports:

and much more. See the .c and .hcc files under regression-tests to see some examples of what it can handle.

TriCera works by encoding the input program into a set of Constrained Horn Clauses (CHCs), which include properties explicitly added to the program through assert and assume statements, but also some implicit properties such as checking the type and runtime safety of heap accesses. It then passes the generated CHCs to Eldarica for solving. This is similar to, for instance, what JayHorn does for Java.

TriCera can also automatically generate function contracts for functions annotated with /*@contract@*/. Contracts will then be generated when the clauses can be solved. See regression-tests/horn-contracts for examples. To print the contracts, -log:3 option must be passed to the tool.

TriCera can parse SV-Comp style task definition files and extract the properties to check from there. The property file must have the same name as the input file except the extension (input_files provided in the property file is currently ignored). Alternatively, the properties to check can be specified via the command-line interface - please refer to tool command-line help for supported properties. By default, TriCera attempts to verify only user-specified assertions, and the unreachability of any calls to reach_error function.

Installation

Since TriCera uses sbt, compilation is quite simple: you just need sbt installed on your machine, and then type sbt assembly to download the compiler, all required libraries, and produce a binary of TriCera.

After compilation (or downloading a binary release), calling TriCera is normally as easy as calling

./tri regression-tests/horn-contracts/fib.hcc

When using a binary release, one can instead also call

java -jar target/scala-2.*/TriCera-assembly*.jar regression-tests/horn-contracts/fib.hcc

A full list of options can be obtained by calling ./tri -h. In particular, the options -cex can be used to show a counterexample when the program is unsafe, and -log:n (n in 1..3) can be used to show the solution when the program is safe.

Try it out online

TriCera has a web interface where you can try it out, which also contains many examples.

Bug reports

TriCera is under development, and bug reports are welcome!

Related papers