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

• A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro and T. Vojnar. Programs with Lists are Counter Automata. In Proc. 18th Intl Conference on Computer Aided Verification (CAV06), LNCS 4144, pp. 517--531. Extended version published as  VERIMAG TR 2006-3.
  

Supported Targets

• DOT the UNIX tool for viewing graphs.
  
• FAST is being developped at LSV (ENS Cachan) and checks for safety properties.
  
• ASPIC 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.
  

Download

Examples

• List Reversal
• List Reversal (expanded version)
• List Counter

Related Projects

• Smallfoot is being developped by the Separation Logic Community (Queen Mary, Imperial College)
  

Contact

Swann Perarnau
Marius Bozga
Radu Iosif