A header-only C++ library for system-level verification and declarative testing of real-time systems with Python bindings.
-
Updated
Apr 6, 2024 - C++
A header-only C++ library for system-level verification and declarative testing of real-time systems with Python bindings.
First-ever high-performance thread-safe BDD library
BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)
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…
STAMINA - the STochiastic Approximate Model-checker for INfinite-state Analysis, integrated with the Storm model checking engine.
metaSMT-Based SMT-LIB2 Consistency Checker
A minimal implementation of an expansion-based QBF solver which does not use recursion.
Tool for creating Timed Automata and checking their language emptiness.
VerC3: Verification Toolkit for C3
An open-source refinement checker for CSP
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.
Linearization of non-linear dynamic systems for reachability analysis
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.
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).
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.
Extendable verification engine and simulator for Tick Tock Automata constructs
This repository provides an extension to the CaDiCaL SAT solver that implements the "DRUPing for Interpolants" algorithm.
Add a description, image, and links to the formal-methods topic page so that developers can more easily learn about it.
To associate your repository with the formal-methods topic, visit your repo's landing page and select "manage topics."