What is L2CA ?
L2CA is a tool for translating programs manipulating singly linked
lists into counter automata. The semantics of the resulting counter
automaton is a bisimulation
of the semantics of the original list program. Consequently, checking
safety and termination properties can be performed on the counter
automaton directly, using existing tools. The results of the analysis
(either positive or negative) of the counter automaton will implicitly
hold on the original program.
- DOT the UNIX tool for viewing graphs.
- FAST is being
developped at LSV (ENS
Cachan) and checks for safety properties.
by Laure Gonnord
(VERIMAG) uses the same input language as FAST and checks for safety
using abstract interpretation.
- ARMC by Andrey Rybalchenko (MPI,
EPFL) checks for safety/termination using abstraction refinement.
The source code of L2CA is available here under Cecill