search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link
automata ltl model-checking program-analysis reachability software-analysis termination

readme

Ultimate

Build Status Jenkins LGPL License

Ultimate is a program analysis framework. Ultimate consists of several plugins that perform steps of a program analysis, e.g., parsing source code, transforming programs from one representation to another, or analyzing programs. Toolchains of these plugins can perform complex tasks, e.g., verify that a C program fulfills a given specification.

The official website includes a web interface which allows you to use several toolchains online, a list of all developers, and a list of awards Ultimate received over the years.

The available documentation can be found in our wiki.

You can download the latest release from GitHub's release page or try our nightly builds.

Developers

The main active developers of Ultimate are:

You can find an extensive list of past and current contributors on our website.

Verification Tools (SV-COMP)

Among other plugins and libraries, Ultimate contains several program verification tools with which we participate in the International Competition on Software Verification (SV-COMP). In this competition, various fully-automatic verifiers and bug finding tools from academia and industry compete, to see which tool can successfully analyse the most programs wrt. a given property. We currently compete with 4 tools: Automizer, Taipan, Kojak and GemCutter.

Ultimate Automizer

Contact: Matthias Heizmann

Automizer uses trace abstraction to generalize infeasibility proofs for single program traces to Floyd-Hoare automata that cover larger parts of the program. For concurrency, it uses a Petri-net-based automata model.

More Information & Web Interface

Publications about Automizer

To cite:

@inproceedings{sas09:trace-abstraction,
  author    = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
  editor    = {Jens Palsberg and Zhendong Su},
  title     = {Refinement of Trace Abstraction},
  booktitle = {Static Analysis, 16th International Symposium, {SAS} 2009, Los Angeles,
               CA, USA, August 9-11, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5673},
  pages     = {69--85},
  publisher = {Springer},
  year      = {2009},
  doi       = {10.1007/978-3-642-03237-0\_7},
}

Ultimate Taipan

Contact: Daniel Dietsch

Taipan uses abstract interpretation with various domains to find loop invariants for path programs. Proofs for path programs are combined using automata operations on Floyd-Hoare-automata. If abstract interpretation cannot find a proof, trace abstraction is used. For concurrency, it uses an explicit product of finite automata.

More Information & Web Interface

Publications about Taipan

To cite:

@inproceedings{sas17:loop-inv-from-ctex,
  author    = {Marius Greitschus and Daniel Dietsch and Andreas Podelski},
  editor    = {Francesco Ranzato},
  title     = {Loop Invariants from Counterexamples},
  booktitle = {Static Analysis - 24th International Symposium, {SAS} 2017, New York,
               NY, USA, August 30 - September 1, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10422},
  pages     = {128--147},
  publisher = {Springer},
  year      = {2017},
  doi       = {10.1007/978-3-319-66706-5\_7}
}

Ultimate Kojak

Contact: Frank Schüssele

Kojak analyses programs using an extension of the Lazy Interpolants CEGAR scheme.

More Information & Web Interface

Publications about Kojak

To cite:

@inproceedings{tacas14:kojak,
  author    = {Evren Ermis and Alexander Nutz and Daniel Dietsch and Jochen Hoenicke and Andreas Podelski},
  editor    = {Erika {\'{A}}brah{\'{a}}m and Klaus Havelund},
  title     = {Ultimate Kojak - (Competition Contribution)},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, {TACAS} 2014,
               Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8413},
  pages     = {421--423},
  publisher = {Springer},
  year      = {2014},
  doi       = {10.1007/978-3-642-54862-8\_36},
}

Ultimate GemCutter

Contact: Dominik Klumpp

GemCutter is a verifier for concurrent programs based on commutativity, i.e., the observation that for certain statements from different threads, the execution order does not matter. It integrates partial order reduction algorithms (that take advantage of commutativity) with a trace abstraction-based CEGAR scheme.

More Information & Web Interface

Publications about GemCutter

To cite:

@inproceedings{pldi22:sound-sequentialization,
  author    = {Azadeh Farzan and Dominik Klumpp and Andreas Podelski},
  editor    = {Ranjit Jhala and Isil Dillig},
  title     = {Sound sequentialization for concurrent program verification},
  booktitle = {{PLDI} '22: 43rd {ACM} {SIGPLAN} International Conference on Programming
               Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022},
  pages     = {506--521},
  publisher = {{ACM}},
  year      = {2022},
  doi       = {10.1145/3519939.3523727},
}

Ultimate Referee

Contact: Frank Schüssele

Referee is a deductive verifier.This means that we check for a program annotated with invariants, if the invariants are sufficient for an inductive proof. For example, for a loop invariant we check if it holds at the beginning of the loop, if it is preserved by the loop body and if it is strong enough the prove the remaining program after the loop correct. These annotated invariants can be extracted from correctness witnesses, therefore Referee can be used as a validator for these.

More Information & Web Interface