Forester—Tool for Verification of Programs with Pointers

News

July, 2019:	Forester is now distributed in a virtual machine. It can be download from Zenodo.
October, 2017:	SV-COMP'18 binary version download here.
November, 2016:	SV-COMP'17 binary version download here.
December 24, 2015:	SV-COMP'16 binary version download 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.

Forester is no longer developed. Its last version, together with source code and the compilation instructions can be found in the virtual machine linked above.

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