fmtools/public
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
main
public/index.html

380 lines
14 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!DOCTYPE html>
<html lang="en-us" dir="ltr">
<head>
<meta name="generator" content="Hugo 0.147.7">
<meta charset="utf-8">
<meta name="viewport" content ="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<title>Formal Methods Tools</title>
<meta name="keywords" content="Formal Methods Tools">
<meta property="og:locale" content='en_US'>
<meta property="og:type" content="article">
<meta property="og:title" content="The Ultimate Formal Methods Toolbox">
<meta property="og:description" content="Welcome to this collection of Formal Methods Tools, which aims to be the world&rsquo;s most comprehensive source for information on tools for formal methods.">
<meta property="og:url" content="https://fmtools.fyi/">
<meta property="og:image" content="images/%!s(&lt;nil&gt;)">
<link rel="canonical" href="https://fmtools.fyi/">
<link rel="apple-touch-icon" sizes="180x180" href='https://fmtools.fyi/apple-touch-icon.png'>
<link rel="icon" type="image/png" sizes="32x32" href='https://fmtools.fyi/favicon-32x32.png'>
<link rel="icon" type="image/png" sizes='16x16' href='https://fmtools.fyi/favicon-16x16.png'>
<link rel="manifest" href='https://fmtools.fyi/site.webmanifest'>
<link rel="stylesheet" href="https://fmtools.fyi/css/styles.256b9fe8f59dcf5eb078f26c8dc26801592eb04b43e5058d5f9b04c2e0e84222d42ff62b207f47e15481a1a1ba359192edeb7bfaac990e44713f5f67852c758f.css" integrity="sha512-JWuf6PWdz16wePJsjcJoAVkusEtD5QWNX5sEwuDoQiLUL/YrIH9H4VSBoaG6NZGS7et7&#43;qyZDkRxP19nhSx1jw==">
<link href="/css/fontawesome.css" rel="stylesheet" />
<link href="/css/brands.css" rel="stylesheet" />
<link href="/css/solid.css" rel="stylesheet" />
<link rel="apple-touch-icon" sizes="57x57" href="/apple-icon-57x57.png">
<link rel="apple-touch-icon" sizes="60x60" href="/apple-icon-60x60.png">
<link rel="apple-touch-icon" sizes="72x72" href="/apple-icon-72x72.png">
<link rel="apple-touch-icon" sizes="76x76" href="/apple-icon-76x76.png">
<link rel="apple-touch-icon" sizes="114x114" href="/apple-icon-114x114.png">
<link rel="apple-touch-icon" sizes="120x120" href="/apple-icon-120x120.png">
<link rel="apple-touch-icon" sizes="144x144" href="/apple-icon-144x144.png">
<link rel="apple-touch-icon" sizes="152x152" href="/apple-icon-152x152.png">
<link rel="apple-touch-icon" sizes="180x180" href="/apple-icon-180x180.png">
<link rel="icon" type="image/png" sizes="192x192" href="/android-icon-192x192.png">
<link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="/favicon-96x96.png">
<link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png">
<link rel="manifest" href="/manifest.json">
<meta name="msapplication-TileColor" content="#ffffff">
<meta name="msapplication-TileImage" content="/ms-icon-144x144.png">
<meta name="theme-color" content="#ffffff">
</head>
<body>
<div class="banner">
<span class="banner-text">
&#x1f6a7; This site is a work in progress. Don&rsquo;t be shy to submit an <a href="https://gitmoss.fyi/fmtools/content/issues/new/choose" target="_blank" >issue</a> or <a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank" >pull request</a> &#x1f6a7;
</span>
</div>
<header>
<h1><a href="/">Formal Methods Tools</a></h1>
<nav>
<ul>
<li>
<a href="/tools/">Tools</a>
</li>
<li>
<a href="/taxonomies/">Data</a>
</li>
<li>
<a href="/about/">About</a>
</li>
</ul>
</nav>
</header>
<main>
<div id="page-header">
<h1>The Ultimate Formal Methods Toolbox</h1>
<span class="subtitle">Discover, Explore, and Contribute to the World’s Largest Collection of Formal Methods Tools</span>
</div>
<section>
<p>Welcome to this collection of Formal Methods Tools, which aims to be the world&rsquo;s most comprehensive source for information on tools for formal methods.
From decades-old classics to cutting-edge tools, this site aims to put as much information as possible into one convenient place.
<a href="/tools" >Explore</a> a wide selection of tools, <a href="/contribute" >contribute</a> tools you make or love, and help grow the formal methods community.</p>
<p>Below are some quick links that may be helpful, plus a random selection of tools (refreshed every time I push updates to this site).</p>
<p><a href="/tools" class="button">
List of Tools
</a>
<a href="/taxonomies" class="button">
Taxonomy Data
</a>
<a href="/contribute" class="button">
Contribute
</a></p>
</section>
<section>
<h2>Try Something New</h2>
<p>This list shows a selection of 20 random tools, refreshed every time this site is updated.</p>
<div id="tool-cards">
<article class="tool-card">
<h3>
Colibri
<span class="subtitle">SMT Solver</span>
</h3>
<p>Colibri is an SMT solver.
</p>
<a href="/tools/sat-smt/colibri/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">Colibri</a>
</article>
<article class="tool-card">
<h3>
Sally
<span class="subtitle">Model Checker</span>
</h3>
<p>Sally is a model checker for infinite state systems described as transition systems.
</p>
<a href="/tools/mc/sally/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">Sally</a>
</article>
<article class="tool-card">
<h3>
CADP
<span class="subtitle">Model Checker</span>
</h3>
<p> [ Closed-Source Tool ]&nbsp; CADP (&ldquo;Construction and Analysis of Distributed …</p>
<a href="/tools/mc/cadp/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">CADP</a>
</article>
<article class="tool-card">
<h3>
Storm
<span class="subtitle">Probabilistic Model Checker</span>
</h3>
<p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.
</p>
<a href="/tools/prob/storm/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">Storm</a>
</article>
<article class="tool-card">
<h3>
MiniSat
<span class="subtitle">SAT Solver</span>
</h3>
<p> [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help …</p>
<a href="/tools/sat-smt/minisat/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">MiniSat</a>
</article>
<article class="tool-card">
<h3>
cvc4
<span class="subtitle">Theorem Prover</span>
</h3>
<p> [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded …</p>
<a href="/tools/sat-smt/cvc4/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">cvc4</a>
</article>
<article class="tool-card">
<h3>
LTSmin
<span class="subtitle">Model Checker</span>
</h3>
<p>LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the …</p>
<a href="/tools/mc/ltsmin/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">LTSmin</a>
</article>
<article class="tool-card">
<h3>
Intrepyd
<span class="subtitle">Model Checker</span>
</h3>
<p> [ Not Maintained Since 2021 ] Intrepyd is a python module that provides a simulator and a model …</p>
<a href="/tools/mc/intrepyd/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">Intrepyd</a>
</article>
<article class="tool-card">
<h3>
veriT
<span class="subtitle">SMT Solver</span>
</h3>
<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …</p>
<a href="/tools/sat-smt/verit/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">veriT</a>
</article>
<article class="tool-card">
<h3>
DSCheck
<span class="subtitle">Model Checker</span>
</h3>
<p>DSCheck is an experimental model checker for testing concurrent OCaml programs.
</p>
<a href="/tools/mc/dscheck/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">DSCheck</a>
</article>
<article class="tool-card">
<h3>
Geyser
<span class="subtitle">Model Checker</span>
</h3>
<p>Geyser is a simple symbolic model checker for propositional transition system systems.
</p>
<a href="/tools/mc/geyser/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">Geyser</a>
</article>
<article class="tool-card">
<h3>
STAMINA
<span class="subtitle">Probabilistic Model Checker</span>
</h3>
<p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces …</p>
<a href="/tools/prob/stamina/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">STAMINA</a>
</article>
<article class="tool-card">
<h3>
E
<span class="subtitle">Theorem Prover</span>
</h3>
<p>E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with …</p>
<a href="/tools/sat-smt/e/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">E</a>
</article>
<article class="tool-card">
<h3>
Bitwuzla
<span class="subtitle">SMT Solver</span>
</h3>
<p>Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …</p>
<a href="/tools/sat-smt/bitwuzla/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">Bitwuzla</a>
</article>
<article class="tool-card">
<h3>
SM(P/)T
<span class="subtitle">Satisfiability Modulo Petri Net</span>
</h3>
<p>SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes …</p>
<a href="/tools/mc/smpt/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">SM(P/)T</a>
</article>
<article class="tool-card">
<h3>
CPAchecker
<span class="subtitle">Model Checker</span>
</h3>
<p> [ Closed-Source Tool ]&nbsp; CPAchecker is a tool for configurable software verification.
</p>
<a href="/tools/mc/cpachecker/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">CPAchecker</a>
</article>
<article class="tool-card">
<h3>
Q3B
<span class="subtitle">SMT Solver</span>
</h3>
<p> [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which …</p>
<a href="/tools/sat-smt/q3b/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">Q3B</a>
</article>
<article class="tool-card">
<h3>
JANI
<span class="subtitle">Quantitative Modeling Specification</span>
</h3>
<p>The JANI specification defines the jani-model model interchange format and the jani-interaction tool …</p>
<a href="/tools/mod/jani/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">JANI</a>
</article>
<article class="tool-card">
<h3>
CGAAL
<span class="subtitle">Model Checker</span>
</h3>
<p>CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game …</p>
<a href="/tools/mc/cgaal/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">CGAAL</a>
</article>
<article class="tool-card">
<h3>
BLAST
<span class="subtitle">Model Checker</span>
</h3>
<p> [ Not Maintained Since 2012 ] BLAST (Berkeley Lazy Abstraction Software verification Tool) is a …</p>
<a href="/tools/mc/blast/" style="position:absolute;top:0;left:0;width:100%;height:100%;z-index:1;text-indent:-9999px;overflow:hidden;">BLAST</a>
</article>
</div>
</section>
<div class="time" style="display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap;">
<div class="footer-links" style="text-align: left;">
Help improve this page!<br/>
Submit an
<a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md&title=[FIX]%20The&#43;Ultimate&#43;Formal&#43;Methods&#43;Toolbox" target="_blank">issue</a> or
<a href="https://gitmoss.fyi/fmtools/content/fork" target="_blank">pull request</a>.
</div>
<div class="footer-date" style="text-align: right;">
Made with &#9829; using <a href="https://gohugo.io" target="_blank">Hugo</a> <br/>
Built <time datetime="2025-06-23T14:04:49-06:00">23 June 2025</time>
</div>
</div>
</main>
<footer>
<p><a href="/contribute">Contribute</a> &nbsp;|&nbsp; <a href="/about">About</a> &nbsp;|&nbsp; <a href="/license">License</a> &nbsp;|&nbsp; <a href="/privacy">Privacy</a> </p>
<p>&copy; Copyright 2025. An open-source project.</p>
</footer>
</body>
</html>
Reference in New Issue View Git Blame Copy Permalink