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.


Supported Targets


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


Related Projects


Swann Perarnau
Marius Bozga
Radu Iosif