A header-only C++ library for system-level verification and declarative testing of real-time systems with Python bindings.

BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)

IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems. IMPaCT is an open-source software tool for the parallelized verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs).

OmegaThreads constructs automatically correct-bu-construction controllers for dynamical systems to satisfy Omega-regular specifications given as discrete parity automata (DPA) or linear temporal logic (LTL) formulae. It constructs a symbolic model of the system and combine it with the specification into a parity game. Winning the parity game res…

First-ever high-performance thread-safe BDD library

Extendable verification engine and simulator for Tick Tock Automata constructs

STAMINA - the STochiastic Approximate Model-checker for INfinite-state Analysis, integrated with the Storm model checking engine.

A tool for parallel computation of interval over-approximations to reachable sets of nonlinear control systems, powered by the pFaces acceleration ecosystem; more briefly, a Parallel Interval Reachability Kernel.

SENSE (Symbolic controlEr Networked SystEms) is a C++ toolbox for constructing symbolic abstractions as well as synthesizing symbolic controllers for networked control systems. The tool has MATLAB and OMNet++ interfaces for closed loop simulation.

VerC3: Verification Toolkit for C3

Linearization of non-linear dynamic systems for reachability analysis

Tool for creating Timed Automata and checking their language emptiness.

metaSMT-Based SMT-LIB2 Consistency Checker

An open-source refinement checker for CSP

A minimal implementation of an expansion-based QBF solver which does not use recursion.

A high-performance library for Mission-time Linear Temporal Logic (MLTL) parsing, Abstract Syntax Tree (AST) manipulation, and formula evaluation. Supports C++ and Python interfaces.

This repository provides an extension to the CaDiCaL SAT solver that implements the "DRUPing for Interpolants" algorithm.