Forester—Tool for Verification of Programs with Pointers
|22nd of March 2011:|| The paper about Forester has been accepted to appear at CAV 2011.|
Forester is a GCC 4.5+ plugin for verification of programs which manipulate complex dynamic data structures. It is based on the well-known CEGAR framework  and represents the set of program states using regular tree automata (for similar approach see ). Note that the tool is an early prototype which handles only a very restricted subset of program constructions.
The plugin uses a new framework for building code analyses developed by Kamil Dudka.
Download the source code of the plugin (included within the distribution of Predator).
Read FAQ included in the archive in order to find out what are the requirements to get things working (mostly related to the compilation of GCC).
Run make build_gcc to download and build GCC 4.5 from sources (if you have more powerful machine and more cores you can try something like make -j5 build_gcc).
Run make to compile the plugin.
Run make check to run some essential tests (if the tests succeed than everything should work properly).
The directory fa_build contains shared library libfa.so which is the compiled plugin. To use it for the verification of a program called foo.c, you can run the gcc in the following way:
gcc-install/bin/gcc -o /dev/null -fplugin=fa_build/libfa.so -c foo.c
The plugin tries to locate the function called main for which the analysis is performed. Note that everything has to be inlined into this function, because function calls are not yet supported.
If you have further questions, do not hesitate to contact authors:
, Lukas Holik
, Adam Rogalewicz
, Jiri Simacek
, and Tomas Vojnar
Forest Automata for Verification of Heap Manipulation
In Proc. of 23rd International Conference on Computer Aided Verification—CAV'11, Cliff Lodge, Snowbird, Utah, USA.
An extended version appeared as the technical report FIT-TR-2011-01
, FIT BUT, Brno, Czech Republic, 2011.
Edmund M. Clarke
, Orna Grumberg
, Somesh Jha
, Yuan Lu
, and Helmut Veith
Counterexample-Guided Abstraction Refinement
In Proc. of 12th International Conference on Computer Aided Verification—CAV'00, Chicago, IL, USA, volume 1855 of LNCS, pages 154–169, 2000. Springer-Verlag.
This work is supported by the Czech Ministry of Education (project COST OC10009, Czech-French Barrande project MEB021023, the long-term institutional project MSM0021630528),
the Czech Science Foundation (projects P103/10/0306, 102/09/H042, 201/09/P531),
the EU/Czech IT4Innovations Centre of Excellence (project ED1.1.00/02.0070),
the European Science Foundation (ESF COST action IC0901),
the French National Research Agency (project ANR-09-SEGI-016 VERIDYC),
and the Brno University of Technology (projects FIT-S-10-1, FIT-S-11-1, FIT-S-12-1).