Personal tools

Implemented Systems

From PUMA Graduiertenkolleg

Jump to: navigation, search

GAVS+ (Game Arena Visualization and Synthesis, Plus!) is an open-source tool which enables to visualize a broad spectrum of algorithmic games used in verification and synthesis, and offers a standard interface with utility functions to establish connection with engineering practice. It is developed by Department of Informatics (Unit 6), TU München, and is served for research and educational purposes. The software is released under the GNU General Public License (v3).

Resource Aware ML (RAML) is a (first-order) functional programming language that fully automatically computes polynomial resource bounds at compile time.

It is based on an automatic type-based amortized analysis that is generic in the resource of interest.

In this prototype implementation we use two machine independent resource metrics: heap-space consumption and evaluation steps in the big-step semantics.

  • PGSolver(Oliver Friedmann and Martin Lange)

The PGSolver library is a collection of algorithms for solving parity games that appear somewhere in the literature, as well as some new heuristics etc. It also defines a standard specification format for parity games as well as winning regions and strategies, and provides a collection of benchmark games.

  • MLSolver(Oliver Friedmann and Martin Lange)

The MLSolver library is a collection of algorithms for solving the satisfiability and validity problems for modal fixpoint logics. It also defines a standard specification format for transition systems, a macro language for defining families of formulas and provides a collection of benchmark problems.

  • CamlDiets(Oliver Friedmann and Martin Lange)

A highly efficient set implementation for fat sets, i.e. densely populated sets over a discrete linear order. Our source code is written in OCaml and implements the Set-interface.

Benchmarks that originate from my research investigating the structure of the strategy improvement algorithm for parity games; used in the crafted category of the SAT competition, 2009.

Nitpick is an open source counterexample generator for Isabelle/HOL that is designed to handle formulas combining (co)inductive datatypes, (co)inductively defined predicates, and (co)recursive functions. It builds on Kodkod, a highly optimized first-order relational model finder developed by the Software Design Group at MIT. The name Nitpick is appropriated from a now retired Alloy precursor.

Sledgehammer is a tool that applies automatic theorem provers (ATPs) and satisfiability-modulo-theories (SMT) solvers on the current goal. The sup- ported ATPs are E, E-SInE, E-ToFoF, LEO-II, Satallax , SNARK, SPASS, Vampire, and Waldmeister. The ATPs are run either locally or remotely via the SystemOnTPTP web service. In addition to the ATPs, the SMT solvers Z3 is used by default, and you can tell Sledgehammer to try CVC3 and Yices as well; these are run either locally or on a server at the TU München.

  • Quickcheck(Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow)

Isabelle/HOLisapopularinteractivetheoremproverbasedonhigher- order logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on resolution provers and SMT solvers for its proof search, the counter- example generator Quickcheck uses the ML compiler as a fast evaluator for ground formulas, and its rival Nitpick is based on the model finder Kodkod, which performs a reduction to SAT. Together with the Isar structured proof format and a new asynchronous user interface, these tools have radically transformed the Isa- belle user experience. This paper provides an overview of the main automatic proof and disproof tools.

HSF is a framework that automates verification of programs. HSF(C) is the instantiation of HSF for verification of C programs. HSF(C) is based on predicate abstraction and refinement following the CEGAR paradigm. There are a number of successful tools including SLAM, Blast, ARMC and CPAChecker that are also based on abstraction refinement. By using abstraction refinement, HSF(C) finds auxiliary assertions required for proving software properties automatically.

DAHL is a Prolog-based compiler and a runtime environment for distributed applications. It aims to provide a high-level specification language in which network protocols can be described as Prolog queries that respond to messages received from the network.

InvGen is an automatic linear arithmetic invariant generator for imperative programs.