Skip to content

Latest commit

 

History

History
196 lines (176 loc) · 19.8 KB

verification_synthesis.md

File metadata and controls

196 lines (176 loc) · 19.8 KB

List of verification and synthesis tools. Please clone, contribute and send pull requests. Minimal markdown knowledge needed to add links:

- [Tool name](link url) (license, coded in language): brief description (Institution/other maintainer)

Please list only Open Source/research tools, proprietary ones are not widely and unconditionally useful. Conditionally (sufficiently) free tools are welcome.

To the extent possible under law, the authors have waived all copyright and related or neighboring rights to this text. You should have received a copy of the CC0 Public Domain Dedication along with this text. If not, see http://creativecommons.org/publicdomain/zero/1.0/.

Model Checking

Closed Systems (Everything controlled)

Explicit

  • SPIN (FUSC, C): LTL model checking for closed systems in Promela (JPL/Caltech, Bell Labs)
    • modex (FUSC, C): C -> Promela: model extractor (JPL/Caltech, Bell Labs)
    • spinja (Apache, Java): Promela model checker (Univ. Twente, TNO)
    • HSF-SPIN: SPIN directed model checking extension [IMT Lucca]
    • Promela -> C (OCaml): translator (Uppsala Univ.)
    • Promela -> C: translator (Univ. Stuttgart)
    • jSpin (GPL-2, Java): GUI for SPIN and Erigone
    • Erigone (GPL-2, Ada): partial SPIN re-implementation for educational purposes
    • EpiSpin: Eclipse plug-in for editing & verifying Promela using Spin (TU Delft)
    • Real-Time SPIN: quantitative dense time SPIN extension using Real-Time Promela (VERIMAG/CNRS)
    • nano-Promela: tools for nano-Promela language
    • promela-metamodel: used to generate Promela from BPEL
  • LTSmin (BSD-3): model checking, LTS minimization, interface to other tools (Univ. Twente)
  • DIVINE-2 (BSD-3): Parallel LTL model checking, DIVINE (Masaryk Univ.)
  • PRISM (GPL-2): Probabilistic Model Checker: discrete/continuous-time Markov chains, timed automata, etc. (Univ. Birmingham, Univ. Oxford)
  • SPOT (GPL, C++/Python): object-oriented model checking library using TGBA
  • JPF (NOSA-1.3): Java model checking & extensions (NASA Ames)
  • HELENA (GPL-2): high-level Petri nets (Paris 13 Univ.)
  • StEAM (C++ ?): C++ model checker (deadlocks, segmentation faults, out of range variables and non-terminating loops) (LS5 Univ. Dortmund)
  • Tulip: LTL model checker of interval Markov chains (recursive also) (Univ. Oxford)
  • PROD (GPL): efficient reachability analysis (Helsinki Univ. Tech.)
  • KBDD: BDD-based satisfiability solver for modal logic K
  • neco (LGPL, Python/Cython): Petri Net compiler & LTL model checker (Univ. d'Evry-Val d'Essonne, Univ. Evry)
  • PEP (GPL-2): modelling and verification framework for parallel systems, interfaces to SPIN, SMV, INA, FC2Tools (SDL, Petri nets)
  • cunf (GPL-3): Toolset for unfolding-based verification of Petri nets extended with read arcs (ENS Cachan)
  • daj (GPL-2, Java): interactive, visual aid for studying execution of distributed algorithms
  • FC2Tools & Autograph: implementation of process algebra theory, verification by compositional reductions and abstraction, explicit/implicit BDD, FC2 file exchange format (INRIA, Ecole des Mines/CMA)
  • ESBMC (BSD-3): context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver (Univ. Southampton)
  • Murphi, original Murphi (BSD-like, C++): enumerative, own input language (Unity style: guard -> action), e.g. used by Microprocessor industry to verify cache coherence protocols (Univ. Utah, Stanford)
    • Eddy Murphi: parallel version of Murphi (Univ. Utah)
    • CMurphy (Univ. Roma)
    • PReach (BSD, Erlang): Distributed Explicit State Model Checker based on Erlang and Murphi (Univ. British Columbia, Intel)
    • MPI Murphi port (Univ. Utah)
  • APMC (FUSC, C/Java): approximate distributed for fully probabilistic systems, PCTL, PLTL (Univ. de Caen Basse-Normandie)

Symbolic

  • NuSMV (LGPL): Symbolic model checking (FBK, CMU, Univ. Genoa, Univ. Trento)
    • NuGAT (LGPL-2+): Game solver on top NuSMV
  • jStar (BSD-3, OCaml): (Queen Mary Univ. London, Cambridge Univ., ETH)
  • coreStar (BSD-3, OCaml): symbolic execution engine for analysis and verification with separation logic (Queen Mary Univ. London, Univ. Cambridge)
  • JSCert JuS: Certified JavaScript (Imperial College, INRIA)
    • jabstr (LGPL, Ocaml): jStar plugin for numerical abstractions
  • LStar (BSD-3, OCaml): automatic prover for programs written in bitcode using separation logic (UCL)
  • VIS: logic circuit simulation, circuit verification, fair CTL model checking, logic synthesis via hierarchy restructuring [UC Berkeley, Univ. Colorado at Boulder, Univ. Texas at Austin]
  • KIND (BSD-3, OCaml): K-induction based for safety properties of Lustre programs, Automatic invariant generation, parallel: PKIND (Univ. Iowa, NASA/CMU, ONERA)
  • Mercury: Parallel Local Sub-CTL Model Checking [LAAS-CNRS]

logic -> automata & automata tools

LTL -> *BA

  • ltl2ba: LTL -> BA (ENS de Cachan)
  • LTL -> NBA (Python)
  • lbtt (GPL): tool for testing programs translating LTL -> BA
  • Wring (Perl): LTL -> GBA (TU Graz)
  • Temporal Massage Parlor: Optimized Translator of an Extended Linear Temporal Logic into Büchi automata and Promela (Bell Labs)
  • LBT: LTL-> BA
  • ltl2tgba: LTL or PSL-> Transition-based GBA | BA (part of SPOT)
  • LTL2AUT (C++): LTL-> BA
  • DBA Minimizer (FUSC, C++): uses external SAT solver for DBA minimization
  • Wring (Perl): translate LTL formulae to generalized Buechi automata (TU Graz)
  • GOAL: graphical interactive tool for defining and manipulating Büchi automata and temporal logic formulae (NTU)

LTL -> DRA

other

Open Systems (Games: System & UnControlled Environment)

  • TuLiP (BSD-3, Python): Receding Horizon Temporal Logic Planning Toolbox (Caltech.CDS)
    • gr1c (BSD-3, C): checking realizability of and synthesizing strategies for GR(1) specifications & much more (Caltech.CDS)
  • LTLMoP (GPL-3, Python): designing, testing, and implementing hybrid controllers generated automatically from task specifications written in Structured English or Temporal Logic (Cornell)
  • Tools from Boston Univ. (?, MATLAB)
  • Tools from Saarland University (Saarland Univ.)
  • PESSOA (FUSC, MATLAB): synthesis of correct-by-design embedded control software based on approximate bisimulations (UCLA)
  • TALIRO (GPL, MATLAB) (ASU)
  • RATSY (LGPL-2+, Python): Requirements Analysis Tool with Synthesis
  • GIST (?): solving probabilistic games with ω-regular objectives qualitatively (IST Austria)
  • JTLV (LGPL-2, Java/C), TLV
  • GAVS+ (GPL-3, Java): visualize algorithmic games used in verification and synthesis (TU Munchen)
  • Anzu (Perl): synthesizes Verilog from LTL (TU Graz)
  • PGSolver (OCaml): tools for generating, manipulating and solving parity games (Univ. Muchich, Univ. Kassel)
  • Sigali (FUSC): Model check implicit labeled transition systems (INRIA)
  • Acacia+ (GPL, Python/C): LTL Realizability check & winning strategy synthesis using AntiChains repo (Univ. Mons), Acacia (GPL-2, Perl)
  • Lily (Perl): synthesizes from PSL | LTL & I/O signal partition, works on top of Wring, outputs VERILOG | dot (TU Graz)
  • PyECDAR (GPL-2, Python): solve timed games based on timed automata models (ITU)
  • Quasy: Quantitative synthesis of reactive systems from qualitative & quantitative GOAL specs, in/out: GOAL format (IST Austria)
  • CADP (FUSC): compilers, equivalence checking tools, model-checkers for temporal logics & μ-calculus, verifications: enumerative, on-the-fly, symbolic using BDD, etc. (INRIA)

Harel StateCharts

Hybrid Systems

  • Ptolemy (BSD-3, Java): modeling, simulation, and design of concurrent, real-time, embedded systems (UC Berkeley)
  • HyTech (FUSC, C): computes condition under which a linear hybrid system satisfies a temporal requirement (UC Berkeley)
  • HyLink (closed, MATLAB): Translates restricted class of Simulink/Stateflow models to hybrid automata (UIUC)
  • HARE (?): Abstraction refinement for safety
  • HTV (closed, MATLAB): verify systems from their simulation and run-time traces using imprecise samples and possibly incomplete models to compute overapproximations of bounded reach sets (UIUC)
  • START: time-bounded static analysis of concurrency properties of Real-Time Embedded Software
  • IF (FUSC): static analysis, model-checking, test generation, Open-Kronos, Kronos: TCTL verification of Timed Automata (VERIMAG)
  • UPPAAL, [UPPAAL-Tiga](http://people.cs.aau.dk/ ̃adavid/tiga/) (FUSC): Timed automata (Uppsala Univ., Aaalborg Univ.)
  • OPAAL (GPL-3, Python): distributed/parallel (discrete time) model checker for networks of timed automata using MPI
  • ECDAR (FUSC): timed interface theory (Aaalborg, INRIA, ITU)
  • SpaceEx (GPL-3): Reachability & safety verification
  • ATAS (GPL-3, Python): Alternating 1-clock (fully decidable) Timed Automata Solver
  • CIF: Compositional Interchange Format for Hybrid Systems toolset
  • CheckMate (MATLAB) modeling, simulation & investigation, demos
  • PPL binding (GPL-2, Python): for Parma Polyhedral Lib features some specific methods for Timed Automata analysis
  • Passel (closed, C#/Python): invariant synthesis and inductive invariant proving (UIUC)
  • TEMPO (FUSC): formal language for modeling distributed systems with (or without) timing constraints as collections of interacting state machines (UIUC)

Theorem Provers

  • PVS (GPL)
  • TPS: (CMU)
  • Coq (INRIA, Ecole Polytechnique, Paris-Sud 11 Univ., Paris Diderot Univ., CNRS)
  • Isabelle (BSD): (Univ. Cabridge, TU Munchen, Univ. Paris-Sud)
  • HOL: Iterative Theorem proving in higher-order logic (Univ. Cambridge)
  • HOL-omega
  • ALF (Univ. Goterborg/Chalmers)
  • Alfa: successor of ALF
  • Agda
  • ACL2: part of Boyer-Moore family of provers (Univ. Texas at Austin)
  • INKA5, INKA: Inductive Theorem Prover
  • Otter & Mace2: first-order and equational logic
  • Prover9 & Mace4: Successors of Otter & Mace2
  • EQP: first-order equational logic: associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search
  • TWELF
  • Maude ITP: Inductive Theorem Prover
  • Mizar
  • PRL: (Cornell)
  • MetaPRL
  • Gandalf
  • E-SETHEO: strategy-parallel compositional theorem prover for first-order logic with equality
  • SPASS: First-Order Logic with Equality (Max Planck Inst. Inf.)
  • Omega (BSD-3): cross between a purely functional programming language and a theorem prover
  • wikipedia list
  • this thread

Runtime Verification

  • MOP (Java): Monitoring-Oriented Programming (UIUC)
  • CHIMP: LTL -> monitors: nondeterministic finite-word automata that accept all illegal executions (Rice Univ.)
  • LTL_3 (GPL): LTL -> Moore FSM monitor
  • TOPL (OCaml): monitor Java programs

Yet un-categorized

  • Maude (UIUC)
    • C-Reducer: Automatic c-reduction of object based modules for the Maude system (IMT Lucca)
    • MESSI: Design, validation and performance evaluation of self-assembly strategies with Maude (IMT Lucca)
    • Circ: automated behavioral prover based on the circularity principle for Maude (UIUC)
  • K: rewrite-based executable semantic framework (UIUC)
  • Matching Logic: regard a language through both operational and axiomatic lenses at the same time (UIUC)
  • Separation logic & local reasoning: wiki & tools list Max Planck Inst. for Soft. Sys.
  • QMRes: Multi-resolution with ZDDs implementation
  • MTSA (Public): Modal Transition Analyser (Imperial College London, Univ. Buenos Aires)

Other tool lists

databases

(non-common) abbreviations

  • FUSC: Free Under Specific Condition (wikipedia term)
  • BA: Buchi Automaton
  • GBA: Generalized BA