Tools & Software

I worked on several research tools & libraries, most of which are available under open source licenses.

• Pareto-Front Enumeration Library (2015)
  This library implements the algorithm described in ArXiV/CoRR 1512.05207 for enumerating all Pareto optima in a multi-dimensional discrete search space where only a monotone oracle function for testing a candidate solution for validity is available. The library is available in Python and C++ and comes with a couple of examples and tests.

• Planet – Neural Network Verification (2017)
  The Planet tool implements the neural network verification approach from my ATVA 2017 paper.

• Slugs – GR(1) Synthesis (2012-2017)
  The Slugs synthesis tool computes reactive systems from the set of generalized reactivity(1) properties. It offers a flexible plug-in framework to incorporate new algorithms and quantitative extensions. It integrates with the LTLMoP robot mission planning framework. A tool paper with details and an introduction to the supported modelling language is available here.
  

  Click here to download the author-archived version of the paper. Copyright by Springer Verlag. The original publication is available at www.springerlink.com

• Bassist – ACTL LTL Synthesis (2012)
  The Bassist tool set synthesizes finite-state systems from linear-time temporal logic (LTL) specifications in which all assumptions and guarantees are also representable in computation tree logic with only universal path quantifiers (ACTL).

• Unbeast – Symbolic Bounded Synthesis (2010-2011)
  Unbeast is a tool for synthesizing finite-state systems from specifications in full linear temporal logic (LTL). The problem is solved in a fully symbolic way. A tool paper explains the implemented approach.
  

  Click here to download the author-archived version of the paper. Copyright by Springer Verlag. The original publication is available at www.springerlink.com

• DBAMinimizer (2010-2011)
  This tool performs minimization of deterministic Büchi automata by reduction to SAT solving. The tool is now a little bit out-of-date as the approach was also implemented by Alexandre Duret-Lutz in the SPOT toolkit.

• NBWMinimizer – Minimization of non-deterministic Büchi automata (2010)
  Performs a more thorough minimization of non-deterministic Büchi automata than other approaches (prior to 2010), using a modified SAT solver and bounded language inclusion checks. The tool bases on the Minisat SAT solver.