ARTMC - Abstract Regular Tree Model Checking

A technique for verification of programs manipulating dynamic data structures.

Basic futures:

Get the full description of the method:

NOTE: A developement of the tool available on this page was supported by the Czech Ministry of Education within the project Security-Oriented Research in Information Technology and by French National Research Agency within th RNTL project AVERILES.


Introduction

ARTMC is a prototype implementation of our fully-automated method for analysing various important properties of programs manipulating dynamic linked data structures - see [1]. We consider non-recursive C programs (with variables over finite data domains) manipulating dynamic linked data structures with possibly several next pointer selectors. The properties we consider are basic consistency of pointer manipulations (no null pointer assignments, no use of undefined pointers, no references to deleted elements). Further undesirable behaviour of the verified programs (e.g., breaking of certain shape invariants such as an introduction of undesirable sharing, cycles, etc.) may be detected via testers written in C and attached to the verified procedures. Then, verification of these properties reduces to reachability of a designated error location.

Our verification method is based on using the generic approach of abstract regular tree model checking (ARTMC) [2]. In regular tree model checking, configurations of the systems being examined are encoded as trees over a suitable ranked alphabet, sets of configurations are described by tree automata, and transitions of the systems are encoded as tree transducers. Subsequently, one computes the set of all configurations reachable from an initial set of configurations by repeatedly applying the tree transducers on the set of the so-far reached configurations (encoded as tree automata). In order to make the method terminate as often as possible and to fight the state explosion problem arising due to increasing sizes of the automata to be handled, various kinds of automatically refinable abstractions over automata are used in ARTMC.

In order to be able to apply ARTMC for verification of programs manipulating dynamic linked data structures, whose configurations (shape graphs) need not be tree-like, we proposed an encoding of shape graphs based on tree automata [1]. We use trees to encode the tree skeleton of a shape graph. The edges of the shape graph that are not directly encoded in the tree skeleton are then represented by routing expressions over the tree skeleton - i.e., regular expressions over directions in a tree (as, e.g., left up, right down, etc.) and the kind of nodes that can be visited on the way. Both the tree skeletons and the routing expressions are automatically discovered by our method. The idea of using routing expressions is inspired by PALE [3] and graph types [4].

Related Publications:
  1. A. Bouajjani, P. Habermehl, A. Rogalewicz, T. Vojnar: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures, SAS 2006 [pdf]
  2. A. Bouajjani, P. Habermehl, A. Rogalewicz, T. Vojnar: Abstract Regular Tree Model Checking, Infinity 2005 [pdf]
  3. J.L. Jensen, M.E. Jorgensen and N. Klarlund and M.I. Schwartzbach: Automatic Verification of Pointer Programs Using Monadic Second-order Logic, PLDI'97.
  4. N. Klarlund and M.I. Schwartzbach: Graph Types, POPL'93.
  5. P. Habermehl, R. Iosif, A. Rogalewicz, T. Vojnar: Proving Termination of Tree Manipulating Programs, ATVA 2007 [link]
  6. R. Iosif and A. Rogalewicz: Automata-based Termination Proofs, CIAA 2009. [link]

1. Requirements

  1. POSIX OS (precompiled binaries available for linux i386)
  2. Python (tested with version 2.4)
  3. Java 1.5
  4. Mona 1.4 - http://www.brics.dk/mona/ (only if you need to build executables from the source code)

2. Licence, Download, Instalation

License GNU GPL v2.1 or any later, see http://www.gnu.org/licenses/gpl.html for more details.

Download ARTMC-distr-2.tgz

Instalation of the precompiled executables (linux i386):

$ tar xzf ARTMC-distr-2.tgz
$ cd ARTMC-distr-2
$ ./set_project_path.sh

Instalation from the source code:

See file INSTALL for more information.


3. Supported program statements


4. Tool Inputs

There are two input files for the tool:

5. Running the tool

To run the tool, you need to perform the following three steps: parse the file program.py to create a set of tree transducers (described as MONA tree automata), parse the file typedefs to create the initial set of configuration (in MONA-style tree automata), and run the ARTMC tool itself.

$ path_to_the_tool/bin/run_generator.t.sh
$ path_to_the_tool/bin/parse_typedef.t.sh
$ path_to_the_tool/bin/main2-[acceleration_method] abstr_height [-ae] [-variance] [-vabstr] [-save]

Acceleration methods:

There are 3 different acceleration methods in the distribution.
main2-predicates
	- Use predicate-based abstraction as a acceleration technique
	- Works for (almost) all examples
main2-fin-height
	- Use finite-height abstraction to accelerate the computation
	- For some examples more effective then predicate-based one.
main2-neighbour
	- Use a neighbour abstraction to accelerate
	- really efective for a limited number of (usually) linked-list examples
	

To run the main part, go to the folder with the example and run 
$ main2- abstr_height [interactive [abstract_everywhere]]

The parameter values:
abstr_height - compulsory parameter
             - initial height of the finite-height abstraction. Usually 1. 
             - no efect for predicates and neighbour - put 1
[-save]      - save all automata at the end	     
[-ae]        - turn on abstraction after each statement (sometimes can lead to better results)

Example:
finite-height with initial height 2, abstract at loop points 
$  path_to_the_tool/bin/main2-fin-height 2
finite-height with initial height 2, abstract everywhere
$  path_to_the_tool/bin/main2-fin-height 2 -ae
predicate based, abstract at loop points
$  path_to_the_tool/bin/main2-predicates 1
predicate based, abstract everywhere
$  path_to_the_tool/bin/main2-predicates 1 -ae

6. Examples

There is a set of "ready to use" examples located in the folder Examples.


7. Authors

Adam Rogalewicz, rogalew@fit.vutbr.cz
Tomas Vojnar, vojnar@fit.vutbr.cz
Pierre Salagnac

Collaborators

Ahmed Bouajjani
Peter Habermehl
Radu Iosif

8. Related Projects


Last changes: 10th November 2009