Formal Methods Tools

All Taxonomy Data

This page contains all of the taxonomy data on this site. There is a lot here, it might be helpful to do a CTRL+F. Click on an item in the first column to focus the view onto one taxonomy (e.g., to view a list of tool developers). Click on a colorful item in the second column to view all the tools for which that term applies (e.g., to view all the tools developed at SRI International).

Applications Constraint Solver Counterexample Generator Hybrid Systems Model Checker Model Generator Modeling Framework Modeling Language Neural Net Verifier Parameter Synthesizer Probabilistic Invariant Synthesizer Probabilistic Model Checker Probabilistic Program Prover Program Prover Program Synthesizer Protocol Verifier Runtime Verifier Rust Verifier SAT Solver SMT Solver Specification Language Static Analyzer Theorem Prover University of Cambridge Visualizer
Developers Leslie Lamport Aalborg University Albert-Ludwigs-Universität Amazon Web Services Bell Labs CEA CNRS ConsenSys CSIRO DHBW Stuttgart DISI-University of Trento Eindhoven University of Technology Federal University of Amazonas Fondazione Bruno Kessler Gilles Audemard Inria INRIA Rhône-Alpes INRIA Rocquencourt Intel Iowa State University ISCAS JetBrains Johannes Kepler Universität Linz Jonathan Nadal LAAS-CNRS Laboratoire Methodes Formelles Laurent Simon Lean FRO LORIA Ludwig-Maximilians-Universität München Masaryk University Matthew Fernandez Microsoft Research MIT Niklas Eén Niklas Sörensson Norbert Manthey OCaml Pro Oxford University PLSE Lab Rocq Team RWTH Aachen Saarland University SRI International Stanford University Technische Universitat Munchen Toccata Tokio TU Wien ULiege Universidad Nacional De Cordoba Universite Paris-Saclay Universite Sorbonne Paris Nord University of Bristol University of Cambridge University of Freiburg University of Illinois University of Iowa University of Lugano University of Manchester University of Nantes University of Oxford University of Southampton University of Stellenbosch University of Twente University of Virginia Uppsala Universitet Uppsala University Utah State University Verimag Vertics
Inputs Agda Alt-Ergo Chyp CNF Cur Dafny DIMACS Galileo GreatSPN HeyVL Isabelle JANI MRMC PNML PRISM PVS Rocq Rust Sally SMTLIB2 WhyML Yices 2
Interfaces .NET C C++ CLI Coq GUI IDE Integration Java Library Online Python Rust VSCode Web Why3
Licenses AGPL-V3 All Rights Reserved Apache-2.0 BSD 4-Clause BSD-2-Clause BSD-3-Clause BSL CRAPL GPL GPL-2.0 GPL-3.0 GPLv2 GPLv3 ISC LGPL LGPL-2.1 LGPLv2 LGPLv2.1 MIT Mozilla-2.0 NASA Open Source OCamlPro-Non-Commercial Unilicense Yolo
Maintenance Actively Maintained Not Maintained
Techniques CDCL GPU