Institute for Computer Languages
Compilers and Languages Group


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


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


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:


[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)


Ioan Drăgan
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2013-02-01 (Webmaster)