The group has developed and contributed to a number of tools and artifacts.

You can try some of our tools online:

• flie: The Formal Language Inference Engine
• Horn-ICE: A learning-based program verifier

Alchemist-CS/DT

Alchemist-CS/DT is a synthesizer for piece-wise linear integer arithmetic expressions from SyGuS specifications, which combines logical constraint solving with decision tree learning

Evrostos: The rLTL Verifier

Evrostos is an efficient, NuSMV-based model checker for rLTL properties. The sources are hosted on GitHub.

ICE Verification Toolkit

ICE is a fully automated program verifier, which extends Microsoft Boogie with various learning-based methods for automatic invariant generation. It has won the invariant synthesis track of the Syntax-Guided Synthesis Competition in 2015 and 2016.

Horn-ICE Verification Toolkit

Horn-ICE is an extension of the ICE tool suite that supports the verification of recursive and concurrent programs. It it also able to synthesize solutions for Constrained Horn clauses. The sources are hosted on GitHub.

libalf

Libalf is a fast, open-source library for learning finite state machines. It implements a wide range of popular active and passive learning algorithms for deterministic and nondeterministic finite automata as well as Moore Machines. The sources are available on GitHub.

QUGA

QUGA (short for Quality Guarantees for Autoencoders) is a tool for the deductive verification of deep auto encoders. The sources are hosted on GitHub.

RESCOT

RESCOT is a C++ tool (with a small Matlab interface) to synthesize resilient controllers for (possibly perturbed) nonlinear control systems with respect to safety and reachability specifications. The sources are available on BitBucket.

Traces2LTL

Traces2LTL is a collection of algorithms for learning LTL formulas from labeled, infinite words (see the flie web demo). The sources are hosted on GitHub.

Horn-ICE Learning for Synthesizing Invariants and Contracts

Tools and benchmarks developed for the paper Horn-ICE Learning for Synthesizing Invariants and Contracts

Invariant Synthesis for Incomplete Verification Engines

Tools and benchmarks developed for the paper Invariant Synthesis for Incomplete Verification Engines