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 . 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) . 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 . 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  and graph types .Related Publications:
$ tar xzf ARTMC-distr-2.tgz $ cd ARTMC-distr-2 $ ./set_project_path.sh
See file INSTALL for more information.
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.