Forest

FramewORk for Embedded System verificaTion

  • startstart
  • downloaddownload
  • TutorialsTutorials
  • PublicationsPublications
  • Try ItTry It
  • Contact usContact us

Download

The version of Forest submitted to the competition can be downloaded executing the following command in a x86_64 machine

wget teisa.unican.es/forest/images/install.sh -O - | bash

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

 

Link1 | Link2 | Link3

Copyright © 2014. All Rights Reserved.

Joomla template created with Artisteer.