LTL Automizer

Ultimate LTL Automizer uses Büchi programs to prove that a C program satisfies an LTL property.
Ultimate LTL Automizer is a toolchain of the Ultimate software analysis framework

Web interface

Ultimate LTL Automizer is available via a web interface.

CAV 2015 Submission "Fairness Modulo Theory: A New Approach to LTL Software Model Checking"

Extended version of the paper

Download the extended version of the paper with a detailed proof in the appendix

Benchmarks

Download the benchmark sets

Command line version

Installation

In order to use LTL Automizer on your machine you require the following:

Usage

After you downloaded LTL Automizer, you can execute it with
./Ultimate LTLAutomizer.xml <inputfile> --settings Default.epf

Your input file should be ANSI C and should contain a main() method. In order to specify an LTL property, you need to add the property to your input file. The syntax is:
//@ ltl invariant <name>: <formula>;
The name of the property should be some string. The formula itself must range over global variables of the program. A formula f has the following syntax:
f := AP(exp) | [] f | <> f | X f | f U f | f R f | f WU f | f || f | !f | f && f | f ==> f | f <==> f
where exp is some boolean expression over global variables of the program. As X, U, R and WU are operators, you cannot use variables with that name in your formula. Also, we currently support only one LTL property per file and run. The analysis will start after the first statement of main() is executed, i.e. all global initialisation will not be taken into account.

Interpreting results

LTL Automizer writes quite some output. At the end, you will see something like this: 

[...]
2015-02-02 16:49:43,110 INFO  [ToolchainManager.java:270]: #######################  End [Toolchain 1] #######################
2015-02-02 16:49:43,110 INFO  [BasicToolchainJob.java:73]:  --- Results ---
2015-02-02 16:49:43,110 INFO  [BasicToolchainJob.java:75]:  * Results from de.uni_freiburg.informatik.ultimate.buchiprogramproduct:
2015-02-02 16:49:43,110 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Initial property automaton
2015-02-02 16:49:43,110 INFO  [BasicToolchainJob.java:95]:     Locations: 2 Edges: 4
2015-02-02 16:49:43,110 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Initial RCFG
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     Locations: 18 Edges: 25
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Initial product
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     Locations: 27 Edges: 57
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Optimized Product
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     Locations: 14 Edges: 28
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:75]:  * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - AllSpecificationsHoldResult: All specifications hold
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     We were not able to verify any specifiation because the program does not contain any specification.
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Ultimate Automizer benchmark data
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     CFG has 18 locations, 0 error locations. Automizer needed 0.0s and 0 iterations. Automata difference [...]
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:75]:  * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer:
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Constructed decomposition of program
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     Your program was decomposed into 1 terminating modules (1 trivial, 0 deterministic, 0 nondeterministic). [...]
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Timing statistics
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     BüchiAutomizer plugin needed 0.1s and 2 iterations. Analysis of lassos took 0.0s. Construction of modules took [...]
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - AllSpecificationsHoldResult: All specifications hold
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:95]:     Büchi Automizer proved that the LTL property F(G(A)) holds
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:75]:  * Results from UltimateCore:
2015-02-02 16:49:43,120 INFO  [BasicToolchainJob.java:89]:   - BenchmarkResult: Toolchain Benchmarks
2015-02-02 16:49:43,130 INFO  [BasicToolchainJob.java:95]:     Benchmark results are:
[...]
2015-02-02 16:49:43,130 INFO  [UltimateCore.java:84]: Preparing to exit Ultimate with return code 0
Closed successfully
The results under Results from de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer: contain the actual result, i.e. in this example, Büchi Automizer proved that the LTL property F(G(A)) holds says that the property was proven successfully.

Changing time and memory limits

This version of LTL Automizer comes with a pre-set timeout of 20 minutes and Java heap space set to 8GB.
If you wish to change the timeout, you must edit Default.epf, search the line /instance/UltimateCore/Toolchain\ timeout\ in\ seconds=1200 and change the 1200 to something else. 0 disables the timeout.
If you want to change the heap space limit, you must edit Ultimate.ini and change the line -Xmx8g to something more appropriate.

Developers

Ultimate LTL Automizer is maintained by Daniel Dietsch, Matthias Heizmann, and Vincent Langenfeld. Just write us an email if you need additional information.