Forester—Tool for Verification of Programs with Pointers

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

News

22nd of March 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.

Acknowledgement

This work is supported by the Barrande programme (MEB021023), the Czech Ministry of Education (COST OC10009, MSM0021630528), the Czech Science Foundation (GD102/09/H042, GP103/10/0306, GP201/09/P531), the European Commission (IC0901), and the Brno University of Technology (FIT-S-10-1).