Lists to Counter Automata


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.

Documentation

Supported Targets

Download

    The source code of L2CA is available here under Cecill free licence.

Examples

Related Projects

Contact

Swann Perarnau
Marius Bozga
Radu Iosif