An open-source refinement checker for CSP
-
Updated
Mar 27, 2017 - C++
An open-source refinement checker for CSP
VerC3: Verification Toolkit for C3
metaSMT-Based SMT-LIB2 Consistency Checker
A minimal implementation of an expansion-based QBF solver which does not use recursion.
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 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.
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…
Extendable verification engine and simulator for Tick Tock Automata constructs
First-ever high-performance thread-safe BDD library
This repository provides an extension to the CaDiCaL SAT solver that implements the "DRUPing for Interpolants" algorithm.
A header-only C++ library for system-level verification and declarative testing of real-time systems with Python bindings.
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).
Tool for creating Timed Automata and checking their language emptiness.
STAMINA - the STochiastic Approximate Model-checker for INfinite-state Analysis, integrated with the Storm model checking engine.
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.
BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)
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."