Forester—Tool for Verification of Programs with Pointers

  1. News
  2. About
  3. Installation
  4. Usage
  5. Contact
  6. Related Papers
  7. Acknowledgement

News

November, 2016:SV-COMP'17 binary version download here.
December 24, 2015:SV-COMP'16 binary versiondownload here.
October 31, 2015:SV-COMP'16 version download here.
June 5, 2013:A paper about Forester extended with ordering relations on data has been accepted to appear at ATVA 2013.
March 6, 2013:An extension of the forest automata framework that performs automatic discovery of boxes has been accepted to appear at CAV 2013.
March 22, 2011:The paper about Forester has been accepted to appear at CAV 2011.

About

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 [1] and represents the set of program states using regular tree automata (for similar approach see [2]). 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.

Installation

  1. Download the source code of the plugin (included within the distribution of Predator).
  2. 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).
  3. 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).
  4. Run make to compile the plugin.
  5. Run make check to run some essential tests (if the tests succeed than everything should work properly).

Usage

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.

Contact

If you have further questions, do not hesitate to contact authors:

[1]
Peter Habermehl, 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.
[2]
Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, and Tomas Vojnar. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In Proc. of 13th International Static Analysis Symposium—SAS'06, Seoul, Korea, volume 4134 of LNCS, pages 52–70, 2006. Springer-Verlag.
[3]
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.

Acknowledgements

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).