- General dynamic linked data structures
- Destructive pointer updates
- Null, undefined and deleted pointer exceptions
- Shape properties
- Fully automated method
- Based on theory of tree languages

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.

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

- A. Bouajjani, P. Habermehl, A. Rogalewicz, T. Vojnar: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures, SAS 2006 [pdf]
- A. Bouajjani, P. Habermehl, A. Rogalewicz, T. Vojnar: Abstract Regular Tree Model Checking, Infinity 2005 [pdf]
- 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.
- N. Klarlund and M.I. Schwartzbach: Graph Types, POPL'93.
- P. Habermehl, R. Iosif, A. Rogalewicz, T. Vojnar: Proving Termination of Tree Manipulating Programs, ATVA 2007 [link]
- R. Iosif and A. Rogalewicz: Automata-based Termination Proofs, CIAA 2009. [link]

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

Download ARTMC-distr-2.tgz

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

See file INSTALL for more information.

- x:=null
- x:=y
- x:=y.next
- x.next=y
- if x==NULL
- if x==y
- if * (nondeterministic branching)
- goto
- exit
- x.next=null
- x.next=new
- x.data="..."
- if x.data=="..."
- x:=random_position
- x=new

- program.py: This file contains a definition of the program in the input format (see Doc/DOC-program.txt)
- typedefs: This file contains a definition of the set of initial configurations (see Doc/DOC-typedefs.txt)

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]

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

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

Tomas Vojnar, vojnar@fit.vutbr.cz

Pierre Salagnac

Peter Habermehl

Radu Iosif

- 3-Valued Logic Analysis Engine (TVLA)
- The Pointer Assertion Logic Engine (PALE)
- Local Reasoning and Separation Logic