Institute for Computer Languages
Compilers and Languages Group

Lingva

Lingva is a tool for generating and proving complex program properties using the recently introduced symbol elimination method.

Download:

A Linux x64 package of our tool can be downloaded from here. In order to invoke our tool one has to run the following command:

./Lingva inputFile.c [OPTIONS]

More details about the supported options, can be found by running

./Lingva --help

Note that in order to run Lingva you need to have Python installed

Examples:

A short C file containing two of the loops from academic benchmarks can be downloaded from here. While the output produced by running Lingva on the first loop can be downloaded from here.

We evaluated Lingva on two sets of benchmarks:

• Academic benchmarks, loops collected from different research papers. These loops can be downloaded from here.
• Open source benchmarks, we collected 150 loops from open source software (bzip, gzip, tar) and tested Lingva on them. These examples are available upon request.

References

[4] Lingva: Generating and Proving Program Properties using Symbol Elimination, Ioan Dragan, Laura Kovacs (PSI 2014) To appear.

[3] Case Studies on Invariant Generation Using a Saturation Theorem Prover, Krystof Hoder, Laura Kovacs, Andrei Voronkov. (MICAI 2011)

[2] Invariant Generation in Vampire, Krystof Hoder, Laura Kovacs, Andrei Voronkov. (TACAS 2011)

[1] Finding Loop Invariants for Programs over Arrays Using a Theorem Prover, Laura Kovacs, Andrei Voronkov. (FASE 2009)

LICENCE