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:
The best way to get started with the tool is to go through one of the following examples:
- ListReversal: ,
- BubbleSort: ,
- InsertSort: ,
- MergeSort: ,
- SelectionSort: ,
Installation instructions
Prerequisites:
- 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. . In Proc. 18th Intl Conference on Computer Aided Verification (CAV06), LNCS 4144, pp. 517—531.
Contributors
- (VERIMAG, Grenoble, France)
- (VERIMAG, Grenoble, France)
- (LIG, Grenoble)
