Verimag

L2CA

a tool for the analysis of pointer programs

 Description

L2CA is a tool for the analysis of pointer programs that manipulate singly-linked list data structures and integer variables. The tool translates an input program with lists into an equivalent integer program, which in turn, can be checked using existing off-the-shelf model checkers.

The supported back-ends are:


 Download

The current version of L2CA is available here: l2ca.tgz

The best way to get started with the tool is to go through one of the following examples:


 Installation instructions

Prerequisites:

  • JAVA version 1.6.0 or later

Unpack the archive and run:

java -jar l2ca.jar initial_configuration_file program_file


 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.

 Contributors

See online : L2CA homepage

Contact | Site Map | Site created with SPIP 2.1.26 + AHUNTSIC [CC License]

Logged in visitors: 10 ; visits: 391003