start
download
Tutorials
Publications
Try It
Contact usDownload
The version of Forest submitted to the competition can be downloaded executing the following command in a x86_64 machine
This should download and execute a script that installs the tool in the current path and performs some tests. A correct installation can be assessed if all tests are correct and terminate in time. The command-line options to be used in svcomp have been condensed to the `-svcomp' parameter. The C file to analyse can be indicated with `-file'.
Forest
Forest implements symbolic execution of LLVM intermediate language and is able to detect errors in programs developed in C. Forest transforms a program into a set of SMT formulas describing each feasible path and decides these formulas with a SMT solver. This enables to prove the satisfiability of reachability conditions such as the ones presented in svcomp. Forest implements different encodings of SMT formulas, according to different theories: linear arithmetic, polynomials and generic bit-accurate and not bit-accurate translations.
Publications
 |
Pablo González de Aledo
Forest |