Fix #15

.gitea/issue_template/add_tool.md

@@ -0,0 +1,44 @@
+---
+name: "Add Tool"
+about: "This template is used to request a new tool be added."
+title: "[ADD] "
+ref: "main"
+assignees: ["mossbiscuits"]
+labels:
+- "new tool"
+- "enhancement"
+projects:
+- "Tool Collection"
+---
+
+Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.
+
+Tool Name: 
+
+Actively maintained? yes/no
+
+Tool Links: (add as many as you need)
+    - [Homepage]()
+    - [Source Code]()
+    - [Online Playground]()
+
+Applications: (think SMT Solver, Theorem Prover, Probabilistic Model Checker, etc.)
+    - 
+
+Developers: (institutions or individuals)
+    - 
+
+Licenses:
+    - 
+
+Input Formats: (think SMTLIB2, DIMACS, etc.)
+    -
+
+Interfaces: (think CLI, GUI, Online, Python Bindings, etc.)
+    -
+
+Publications: (a DOI or URL is sufficient)
+    - 
+
+Additional Details or Description:
+

.gitea/issue_template/fix_tool.md

@@ -0,0 +1,42 @@
+---
+name: "Fix Tool"
+about: "This template is used to request a new tool be fixed."
+title: "[FIX] "
+ref: "main"
+assignees: ["mossbiscuits"]
+labels:
+- "fix tool"
+- "bug"
+---
+
+Fill in as little or as much information as you like, but more information increases my ability to add your tool effectively.
+
+Tool Name: 
+
+Actively maintained? yes/no
+
+Tool Links: (add as many as you need)
+    - [Homepage]()
+    - [Source Code]()
+    - [Online Playground]()
+
+Applications: (think SMT Solver, Theorem Prover, Probabilistic Model Checker, etc.)
+    - 
+
+Developers: (institutions or individuals)
+    - 
+
+Licenses:
+    - 
+
+Input Formats: (think SMTLIB2, DIMACS, etc.)
+    -
+
+Interfaces: (think CLI, GUI, Online, Python Bindings, etc.)
+    -
+
+Publications: (a DOI or URL is sufficient)
+    - 
+
+Additional Details or Description:
+

_index.md

@@ -2,6 +2,7 @@
 title = 'The Ultimate Formal Methods Toolbox'
 subtitle = 'Discover, Explore, and Contribute to the World’s Largest Collection of Formal Methods Tools'
 # date = 2023-01-01T08:00:00-07:00
+date = 2025-06-07
 # draft = false 
 +++
 
@@ -11,11 +12,11 @@ From decades-old classics to cutting-edge tools, this site aims to put as much i
 
 Below are some quick links that may be helpful, plus a random selection of tools (refreshed every time I push updates to this site). 
 
-{{<button href="/applications/smt-solver/">}}
-SMT Solvers
+{{<button href="/tools">}}
+List of Tools
 {{</button>}} 
-{{<button href="/applications/model-checker/">}}
-Model Checkers
+{{<button href="/taxonomies">}}
+Taxonomy Data
 {{</button>}} 
 {{<button href="/contribute">}}
 Contribute

about.md

@@ -1,10 +1,10 @@
 +++
 title = 'About'
 subtitle = 'Learn more about the Formal Methods Tools project'
+date = 2025-06-07
 +++
 
-
-The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. Our goal is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.
+The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. The goal of this website is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.
 
 ## Key Objectives
 

contribute.md

@@ -1,5 +1,12 @@
 +++
 title = 'Contribute'
+date = 2025-06-07
 +++
 
-Instructions coming soon. Please see https://gitmoss.fyi/fmtools/content/wiki/Contribute for temporary instructions.
+Instructions coming soon. Please see https://gitmoss.fyi/fmtools/content/wiki/Contribute for temporary instructions.
+
+## Quick Links
+
+- Request addding a tool: [Submit Git Issue](https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2fadd_tool.md)
+- Request fixing a tool: [Submit Git Issue](https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md)
+

license.md

@@ -1,6 +1,7 @@
 +++
 title = 'MIT License'
 subtitle = 'Open-Source and Free to Use'
+date = 2025-06-07
 +++
 
 MIT License

privacy.md

@@ -1,12 +1,13 @@
 +++
 title = 'Privacy'
 subtitle = "tl;dr: I won't know you were here."
+date = 2025-06-07
 +++
 
-This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and 
+This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and there is no money to be made from this project.
 
-If you choose to contribute content (such as submitting an article or comment), any information you voluntarily provide will be stored as part of the website's content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website's owner. Any information you voluntarily provide as part of a code contribution becomes public information and may be used by the general public as allowed by respective laws and policies.
+If you choose to contribute content (including emails, issues, and pull requests), any information you voluntarily provide may be stored as part of the website's content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website's owner. Due to the public nature of its disclosure, this information is not considered private and may be used by the general public as allowed by respective laws and policies. Your privacy is respected, and no unnecessary data is collected or shared. 
 
-Your privacy is respected, and no unnecessary data is collected or shared. If you or your tool is listed on this page and you would like to remove it, please contact `fmtools@mossbiscuits.com` with the subject `Please remove my data`.
+If your information (e.g., your name, a tool you developed, or an attribution) is listed on this website and you would like to remove it, please contact `fmtools@mossbiscuits.com` with the subject `Please remove my data`. I cannot make guarantees, but I will make a reasonable effort to remove or redact your information within 1-3 business days.
 
-*Look at you, reading privacy policies. Thanks for being a responsible internet user.*
+*Look at you, reading privacy policies. Thanks for being a responsible internet user. Now go do something more interesting* :slightly_smiling_face:

tools/mc/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Model Checking Tools"
+layout = "section"
++++
+
+This page lists all of the model checking tools on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/mc/blast.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'BLAST'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://forge.ispras.ru/projects/blast", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala Universitet', 'Aalborg University']
+licenses = ['Apache-2.0']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2012">}}
+BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution.

tools/mc/cadp.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CADP'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://cadp.inria.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['INRIA Rocquencourt']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+{{<closed-source>}}
+CADP ("Construction and Analysis of Distributed Processes", formerly known as "CAESAR/ALDEBARAN Development Package") is a toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, web services, etc. 

tools/mc/cgaal.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CGAAL'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/d702e20/CGAAL", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['University of Twente']
+licenses = ['AGPL-v3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+CGAAL is a model checker of alternating-time temporal logic (ATL) properties on concurrent game structures (CGSs).

tools/mc/concuerror.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Concuerror'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "http://parapluu.github.io/Concuerror", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/parapluu/Concuerror", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala University']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Concuerror is a stateless model checking tool for Erlang programs.

tools/mc/cpachecker.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CPAchecker'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://cpachecker.sosy-lab.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://gitlab.com/sosy-lab/software/cpachecker/", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Ludwig-Maximilians-Universität München']
+licenses = ['Apache-2.0']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+{{<closed-source>}}
+CPAchecker is a tool for configurable software verification.

tools/mc/dscheck.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'DSCheck'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/ocaml-multicore/dscheck", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Twente']
+licenses = ['ISC']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+DSCheck is an experimental model checker for testing concurrent OCaml programs.

tools/mc/eldarica.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Eldarica'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/uuverifiers/eldarica", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala University']
+licenses = ['BSL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Eldarica is a model checker for Horn clauses, Numerical Transition Systems, and software programs.

tools/mc/esbmc.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'ESBMC'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://ssvlab.github.io/esbmc/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/esbmc/esbmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Federal University of Amazonas', 'University of Bristol', 'University of Manchester', 'University of Stellenbosch', 'University of Southampton']
+licenses = ['Apache-2.0', 'BSD 4-clause', 'MIT', 'BSD 3-clause', 'GPLv3', ]
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+ESBMC is a context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs.

tools/mc/geyser.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Geyser'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/JakubSarnik/geyser", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Eindhoven University of Technology']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+techniques = ['PDR', 'CAR']
+# publications = ['']
++++
+
+Geyser is a simple symbolic model checker for propositional transition system systems.

tools/mc/imitator.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'IMITATOR'
+subtitle = 'Parameter Synthesis'
+links = [
+    { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Parameter Synthesizer']
+developers = ['Universite Sorbonne Paris Nord']
+licenses = ['GPLv3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more. 

tools/mc/imspin.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'ImSpin'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/MrDiver/ImSpin", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Eindhoven University of Technology']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['PDR', 'CAR']
+# publications = ['']
++++
+
+ImSpin is a frontend for the [SPIN](../spin) model checker, providing an environment for users engaged in model checking tasks.

tools/mc/intrepyd.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Intrepyd'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/formalmethods/intrepid", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2021">}}
+Intrepyd is a python module that provides a simulator and a model checker in form of a rich API, to allow the rapid prototyping of formal methods algorithms for the rigorous analysis of circuits, specifications, models.

tools/mc/ivy.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'IVy'
+subtitle = 'Protocol Verifier'
+links = [
+    { title = "Homepage", url = "https://kenmcmil.github.io/ivy/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/kenmcmil/ivy", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Protocol Verifier']
+developers = ['Microsoft Research']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2023">}}
+IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques.

tools/mc/kind2.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Kind 2'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://kind2-mc.github.io/kind2/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/kind2-mc/kind2", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Iowa']
+licenses = ['Apache-2.0']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Kind 2 is a multi-engine SMT-based automatic model checker for synchronous reactive systems.

tools/mc/ltsa.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'LTSA'
+subtitle = 'Labelled Transition System Analyser'
+links = [
+    { title = "Homepage", url = "https://www.doc.ic.ac.uk/ltsa/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['University of Twente']
+# licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2018">}}
+LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour. 

tools/mc/ltsmin.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'LTSmin'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/utwente-fmt/ltsmin", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Twente']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+LTSmin started out as a generic toolset for manipulating labelled transition systems. Meanwhile the toolset was extended to a a full (LTL/CTL/μ-calculus) model checker, while maintaining its language-independent characteristics.

tools/mc/mcltlrs.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'mcltl-rs'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/NotBad4U/mcltl-rs", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Fondazione Bruno Kessler']
+# licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2020">}}
+<!-- {{<closed-source>}} -->
+mcltl-rs is an experimental model checker for LTL written in Rust.

tools/mc/mcrl2.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'mCRL2'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/mCRL2org/mCRL2", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Eindhoven University of Technology']
+licenses = ['BSL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.

tools/mc/mercury.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Mercury'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://mcrl2.org", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/rtsaad/mercury", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['LAAS-CNRS', 'Vertics']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2020">}}
+Mercury is a Model Checker developed for multicore, multiprocessors machine with shared memory.

tools/mc/munta.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'MUNTA'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/wimmers/munta", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2020">}}
+MUNTA is a model checker for the popular realtime systems modeling formalism of Timed Automata

tools/mc/nusmv.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'NuSMV'
+subtitle = 'Symbolic Model Checker'
+links = [
+    { title = "Homepage", url = "https://nusmv.fbk.eu/index.html", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Fondazione Bruno Kessler']
+licenses = ['LGPL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2018">}} -->
+NuSMV is a symbolic model checker.

tools/mc/nuxmv.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'NuXMV'
+subtitle = 'Symbolic Model Checker'
+links = [
+    { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Fondazione Bruno Kessler']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2018">}} -->
+{{<closed-source>}}
+nuXmv is a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.

tools/mc/pnmc.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Pnmc'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "http://ltsmin.utwente.nl/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['University of Twente']
+licenses = ['BSD']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Pnmc is a symbolic model checker for Petri nets.

tools/mc/pypl.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'pyPL'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/nclarius/pyPL", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker', 'Model Generator', 'Theorem Prover']
+developers = ['Matthew Fernandez']
+licenses = ['Unilicense']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+pyPL is a naive model generator, model checker and theorem prover.

tools/mc/romeo.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Roméo'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://romeo.ls2n.fr/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/ahamez/pnmc", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['University of Nantes']
+licenses = ['GPL']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2018">}} -->
+<!-- {{<closed-source>}} -->
+Romeo allows the modelling of complex systems using extensions of time Petri nets.

tools/mc/rumur.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Rumur'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/Smattr/rumur", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Matthew Fernandez']
+licenses = ['Unilicense']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+Rumur is a model checker.

tools/mc/sally.md

@@ -0,0 +1,24 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Sally'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "http://sri-csl.github.io/sally/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/SRI-CSL/sally", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['SRI International']
+licenses = ['GPLv2']
+inputs = ['Sally']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2023">}} -->
+
+
+Sally is a model checker for infinite state systems described as transition systems.

tools/mc/smpt.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'SM(P/)T'
+subtitle = 'Satisfiability Modulo Petri Net'
+links = [
+    # { title = "Homepage", url = "https://www.imitator.fr/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/nicolasAmat/SMPT", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['LAAS-CNRS']
+licenses = ['GPLv3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

tools/mc/spaceex.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'SpaceEx'
+subtitle = 'Hybrid Systems'
+links = [
+    { title = "Homepage", url = "http://spaceex.imag.fr/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://forge.ispras.ru/projects/blast/repository", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Hybrid Systems']
+developers = ['Verimag']
+licenses = ['GPLv3']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification in continuous and hybrid systems.

tools/mc/spin.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Spin'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://spinroot.com/spin/whatispin.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/nimble-code/Spin", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Bell Labs']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['PDR', 'CAR']
+# publications = ['']
++++
+
+Spin is a model checker for multi-threaded software.

tools/mc/stateright.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'stateright'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://docs.rs/stateright/latest/stateright/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/stateright/stateright", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Jonathan Nadal']
+licenses = ['MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+`stateright` is a Rust library for model checking systems, with an emphasis on distributed systems.

tools/mc/tapaal.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'TAPAAL'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://www.tapaal.net/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Aalborg University']
+licenses = ['Open Source 3.0', 'BSD', 'GPLv2']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+TAPAAL is a tool for verification of timed-arc petri nets

tools/mc/timesolver.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'TimeSolver'
+subtitle = 'Model Checker'
+links = [
+    # { title = "Homepage", url = "https://nuxmv.fbk.eu/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/jkeiren/TimeSolver", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+# developers = ['Fondazione Bruno Kessler']
+# licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<inactive year="2019">}}
+TimeSolver is a Model Checker for timed automata that uses pes (predicate equation systems).

tools/mc/uppaal.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Uppaal'
+subtitle = 'Model Checker'
+links = [
+    { title = "Homepage", url = "https://uppaal.org/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/imitator-model-checker/imitator", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['Uppsala Universitet', 'Aalborg University']
+licenses = ['All Rights Reserved']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+{{<closed-source>}}
+Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).

tools/mod/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Modeling (Tools and Languages)"
+layout = "section"
++++
+
+This page lists all of the modeling tools and Languages on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/mod/jani.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'JANI'
+subtitle = 'Quantitative Modeling Specification'
+links = [
+    { title = "Homepage", url = "https://momba.dev/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/koehlma/momba", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Modeling Language']
+developers = ['University of Twente', 'RWTH Aachen', 'ISCAS', 'Universidad Nacional de Cordoba']
+licenses = ['Apache-2.0', 'MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol.

tools/mod/momba.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Momba'
+subtitle = 'Quantitative Modeling Framework'
+links = [
+    { title = "Homepage", url = "https://momba.dev/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/koehlma/momba", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Modeling Framework']
+developers = ['Saarland University']
+licenses = ['Apache-2.0', 'MIT']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+Momba is a Python framework for dealing with quantitative models centered around the [JANI-model](../jani) interchange format.

tools/mod/tlaplus.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'TLA+'
+subtitle = 'Modeling Language'
+links = [
+    { title = "Homepage", url = "https://lamport.azurewebsites.net/tla/tla.html", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/TAPAAL/", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Modeling Language']
+developers = [' Leslie Lamport']
+licenses = ['Open Source 3.0', 'BSD', 'GPLv2']
+# inputs = ['Sally']
+# interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2012">}} -->
+<!-- {{<closed-source>}} -->
+TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.

tools/prob/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Probabilistic Tools"
+layout = "section"
++++
+
+This page lists all of the probabilistic tools on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/prob/caesar.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Caesar'
+subtitle = 'Probabilistic Program Prover'
+links = [
+    { title = "Homepage", url = "https://www.caesarverifier.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/caesar", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Program Prover']
+developers = ['RWTH Aachen']
+licenses = ['MIT']
+inputs = ['HeyVL']
+interfaces = ['CLI', 'VSCode']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Caesar is a deductive verifier for probabilistic programs.

tools/prob/comics.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'COMICS'
+subtitle = 'DTMC Counterexample Generator'
+links = [
+    { title = "Homepage", url = "https://ths.rwth-aachen.de/research/tools/comics/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Counterexample Generator']
+developers = ['RWTH Aachen']
+# licenses = ['GPLv3']
+# inputs = ['PRISM', 'JANI', 'PNML', 'GreatSPN', 'Galileo', 'MRMC']
+# interfaces = ['CLI', 'C++', 'Python']
+# maintenance = ['Unknown']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for discrete-time Markov Chains (DTMCs).

tools/prob/dftgui.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'DFT Visualization'
+subtitle = 'Visualization for Dynamic Fault Trees'
+links = [
+    { title = "Homepage", url = "https://moves-rwth.github.io/dft-gui/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/dft-gui", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Visualizer']
+developers = ['RWTH Aachen']
+# licenses = ['MIT']
+# inputs = ['HeyVL']
+interfaces = ['GUI', 'Online']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+{{<inactive year="2021">}}
+PRINSYS is a tool for invariant generation for probabilistic programs.

tools/prob/prinsys.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'PRINSYS'
+subtitle = 'PRobabilistic INvariant SYnthesiS'
+links = [
+    { title = "Homepage", url = "https://www-i2.informatik.rwth-aachen.de/prinsys/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/moves-rwth/caesar", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Invariant Synthesizer']
+developers = ['RWTH Aachen']
+# licenses = ['MIT']
+# inputs = ['HeyVL']
+interfaces = ['GUI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+{{<inactive year="2012">}}
+PRINSYS is a tool for invariant generation for probabilistic programs.

tools/prob/prism.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'PRISM'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://prismmodelchecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Oxford University']
+licenses = ['GPLv2']
+inputs = ['PRISM', 'MRMC']
+interfaces = ['CLI', 'Java']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Kwiatkowska2011']
++++
+
+<!-- {{<inactive year="2023">}} -->
+PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.

tools/prob/prophesy.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Prophesy'
+subtitle = 'Parameter Synthesis'
+links = [
+    # { title = "Homepage", url = "https://www-i2.informatik.rwth-aachen.de/prinsys/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/prophesy", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Parameter Synthesizer']
+developers = ['RWTH Aachen']
+licenses = ['GPLv3']
+# inputs = ['HeyVL']
+# interfaces = ['GUI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Hensel2022']
++++
+
+{{<inactive year="2019">}}
+Prophesy is a tool set for parameter synthesis of parametric Markov models.

tools/prob/stamina.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'STAMINA'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://staminachecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://staminachecker.org/source.html", icon = 'fa-brands fa-github'  },
+    { title = "Playground", url = "https://staminachecker.org/run.html", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Utah State University']
+licenses = ['MIT', 'GPLv3']
+inputs = ['PRISM']
+interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Jeppson2023']
++++
+
+<!-- {{<inactive year="2023">}} -->
+ A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either [Storm](../storm) or [PRISM](../prism).

tools/prob/storm.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Storm'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://www.stormchecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['RWTH Aachen']
+licenses = ['GPLv3']
+inputs = ['PRISM', 'JANI', 'PNML', 'GreatSPN', 'Galileo', 'MRMC']
+interfaces = ['CLI', 'C++', 'Python']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Hensel2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Storm is a tool for the analysis of systems involving random or probabilistic phenomena. 

tools/programs/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Program Proof Tools"
+layout = "section"
++++
+
+This page lists all of the program proof tools on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/programs/aeneas.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Aeneas'
+subtitle = 'Rust Verifier'
+links = [
+    { title = "Homepage", url = "https://aeneasverif.github.io/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/AeneasVerif/aeneas", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Program Prover', 'Rust Verifier']
+developers = ['Microsoft Research', 'Inria']
+licenses = ['Apache-2.0']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Aeneas (pronunced [Ay-nay-as]) is a verification toolchain for Rust programs.

tools/programs/creusot.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Creusot'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://dafny.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/creusot-rs/creusot", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Program Prover', 'Rust Verifier']
+# developers = ['Amazon Web Services']
+licenses = ['LGPLv2.1']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Creusot is a deductive verifier for Rust code.

tools/programs/dafny.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Dafny'
+subtitle = 'Program Proofs'
+links = [
+    { title = "Homepage", url = "https://dafny.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/dafny-lang/dafny", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Program Prover']
+developers = ['Amazon Web Services']
+licenses = ['MIT']
+inputs = ['Dafny']
+interfaces = ['CLI', 'VSCode']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Dafny is a verification-aware programming language that has native support for recording specifications and is equipped with a static program verifier.

tools/programs/kani.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Kani'
+subtitle = 'Rust Verifier'
+links = [
+    { title = "Homepage", url = "https://model-checking.github.io/kani/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/model-checking/kani", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker', 'Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['Apache-2.0', 'MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+The Kani Rust Verifier is a bit-precise model checker for Rust.

tools/programs/loom.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Loom'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/tokio-rs/loom", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+developers = ['Tokio']
+licenses = ['MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Loom is a testing tool for concurrent Rust code. 

tools/programs/miri.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Miri'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://model-checking.github.io/kani/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/rust-lang/miri", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['Apache-2.0', 'MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Miri is an Undefined Behavior detection tool for Rust.

tools/programs/prusti.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Prusti'
+subtitle = 'Rust Verifier'
+links = [
+    { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/viperproject/prusti-dev", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['Mozilla-2.0']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+{{<inactive year="2024">}}
+Prusti is a prototype verifier for Rust that makes it possible to formally prove absence of bugs and correctness of code contracts.

tools/programs/shuttle.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Loom'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/awslabs/shuttle", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+developers = ['Amazon Web Services']
+licenses = ['MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Shuttle is a library for testing concurrent Rust code.

tools/programs/verus.md

@@ -0,0 +1,22 @@
++++
+date = 2025-07-10
+draft = false
+title = 'Verus'
+subtitle = 'Rust Verifier'
+links = [
+    # { title = "Homepage", url = "https://www.pm.inf.ethz.ch/research/prusti.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/verus-lang/verus", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Rust Verifier']
+# developers = ['Microsoft Research', 'Inria']
+licenses = ['MIT']
+inputs = ['Rust']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Verus is a tool for verifying the correctness of code written in Rust.

tools/sat-smt/_index.md

@@ -0,0 +1,10 @@
++++
+title = "SAT & SMT Tools"
+layout = "section"
++++
+
+This page lists all of the SAT & SMT tools on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/sat-smt/alt-ergo.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Alt-Ergo'
+subtitle = 'SMT Solver'
+links = [
+    { title = "Homepage", url = "https://alt-ergo.ocamlpro.com/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/ocamlpro/alt-ergo", icon = 'fa-brands fa-github'  },
+    { title = "Playground", url = "https://try-alt-ergo.ocamlpro.com/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver']
+developers = ['OCaml Pro']
+licenses = ['OCamlPro-Non-Commercial']
+inputs = ['SMTLIB2', 'Alt-Ergo']
+interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat. 

tools/sat-smt/bitwuzla.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Bitwuzla'
+subtitle = 'SMT Solver'
+links = [
+    { title = "Homepage", url = "https://bitwuzla.github.io", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/bitwuzla/bitwuzla", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver']
+developers = ['Stanford University']
+licenses = ['MIT']
+inputs = ['SMTLIB2']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Niemetz2023']
++++
+
+<!-- {{<inactive year="2024">}} -->
+Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.

tools/sat-smt/boolector.md

@@ -0,0 +1,23 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Boolector'
+subtitle = 'SMT Solver'
+links = [
+    { title = "Homepage", url = "https://boolector.github.io/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/boolector/boolector", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver']
+developers = ['Stanford University', 'Johannes Kepler Universität Linz']
+licenses = ['MIT']
+inputs = ['SMTLIB2']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+publications = ['Niemetz2014']
++++
+
+{{<inactive year="2024">}}
+Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
+Succeeded by [Bitwuzla](../bitwuzla)

tools/sat-smt/cadical.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CaDiCaL'
+subtitle = 'SAT Solver'
+links = [
+    # { title = "Homepage", url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/arminbiere/cadical", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SAT Solver']
+developers = ['University of Freiburg']
+licenses = ['MIT']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+CaDiCaL is a simplified satisfiability solver.

tools/sat-smt/colibri.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Colibri'
+subtitle = 'SMT Solver'
+links = [
+    { title = "Homepage", url = "https://colibri.frama-c.com/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://git.frama-c.com/pub/colibrics/-/tree/master", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver']
+developers = ['CEA']
+licenses = ['MIT']
+inputs = ['SMTLIB2']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+Colibri is an SMT solver.

tools/sat-smt/cryptominisat.md

@@ -0,0 +1,33 @@
++++
+date = 2025-06-07
+draft = false
+title = 'CryptoMiniSat'
+subtitle = 'SAT Solver'
+links = [
+    { title = "Homepage", url = "https://www.msoos.org/cryptominisat5/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/msoos/cryptominisat", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc4.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SAT Solver']
+developers = ['INRIA Rhône-Alpes', 'University of Virginia']
+licenses = ['MIT', 'GPLv2']
+inputs = ['CNF']
+interfaces = ['CLI', 'Python', 'C++', ]
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Soos2009']
++++
+
+<!-- {{<inactive year="2021">}} -->
+CryptoMiniSat is a SAT solver.
+
+## APIs and Bindings
+This tool is available through the following interfaces:
+
+- **C++ Namespace:** Documentation on [homepage](https://www.msoos.org/cryptominisat5/)
+- **Python package:** [PyPI package](https://pypi.org/project/pycryptosat/)
+<!-- - **.NET API:** [Z3 .NET Namespace Reference](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html) -->
+<!-- - **Java API:** [Z3 Java API Reference](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html) -->
+<!-- - **Rust bindings:** [z3 crate on crates.io](https://crates.io/crates/z3) -->
+
+

tools/sat-smt/cvc4.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'cvc4'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://cvc4.github.io/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/CVC4/CVC4-archived", icon = 'fa-brands fa-github'  },
+    { title = "Playground", url = "https://cvc4.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver', 'Theorem Prover']
+developers = ['Stanford University', 'University of Iowa']
+licenses = ['BSD']
+inputs = ['SMTLIB2']
+interfaces = ['CLI', 'Online']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+publications = ['Barrett2011']
++++
+
+{{<inactive year="2021">}}
+cvc4 is an automatic theorem prover for SMT problems. It is succeeded by [cvc5](../cvc5)

tools/sat-smt/cvc5.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'cvc5'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://cvc5.github.io/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/cvc5/cvc5", icon = 'fa-brands fa-github'  },
+    { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver', 'Theorem Prover']
+developers = ['Stanford University', 'University of Iowa']
+licenses = ['BSD']
+inputs = ['SMTLIB2']
+interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+cvc5 is an automatic theorem prover for SMT problems.

tools/sat-smt/dreal.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'dReal'
+subtitle = 'SMT Solver'
+links = [
+    { title = "Homepage", url = "https://dreal.github.io/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/dreal/dreal4", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver']
+# developers = ['Johannes Kepler Universität Linz']
+licenses = ['Apache-2.0']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+{{<inactive year="2023">}}
+dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions. 

tools/sat-smt/e.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'E'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/eprover/eprover", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover']
+developers = ['DHBW Stuttgart']
+licenses = ['GPLv2']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with equality.

tools/sat-smt/lean.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'LEAN'
+subtitle = 'Programming Language & Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://lean-lang.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/leanprover/lean4", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover', 'Modeling Language']
+developers = ['Lean FRO']
+licenses = ['Apache-2.0']
+# inputs = ['SMTLIB2']
+# interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+cvc5 is an automatic theorem prover for SMT problems.

tools/sat-smt/lingeling.md

@@ -2,7 +2,7 @@
 date = 2025-06-07
 draft = false
 title = 'Lingeling'
-subtitle = 'SMT Solver'
+subtitle = 'SAT Solver'
 links = [
     { title = "Homepage", url = "https://fmv.jku.at/lingeling/", icon = 'fa-solid fa-home' },
     { title = "Source Code", url = "https://github.com/arminbiere/lingeling", icon = 'fa-brands fa-github'  },

tools/sat-smt/mathsat.md

@@ -10,7 +10,7 @@ links = [
 ]
 applications = ['SMT Solver']
 developers = ['Fondazione Bruno Kessler','DISI-University of Trento']
-licenses = ['All rights reserved']
+licenses = ['All Rights Reserved']
 # inputs = ['']
 interfaces = ['CLI']
 maintenance = ['Actively Maintained']
@@ -19,4 +19,4 @@ maintenance = ['Actively Maintained']
 +++
 
 {{<closed-source>}}
-MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. 
+MathSAT is an SMT solver supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally).

tools/sat-smt/vampire.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Vampire'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://vprover.github.io/index.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/vprover/vampire", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover']
+developers = ['TU Wien']
+licenses = ['BSD']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+Vampire is a theorem prover.

tools/sat-smt/zipperposition.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Zipperposition'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://sneeuwballen.github.io/zipperposition/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/sneeuwballen/zipperposition", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Theorem Prover']
+developers = ['TU Wien']
+licenses = ['BSD']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+Zipperposition is an automated theorem prover for first-order logic with equality and theories.

tools/termination/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Termination Tools"
+layout = "section"
++++
+
+This page lists all of the termination tools on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/termination/approve.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = true
+title = 'AProVE TODO'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://cvc5.github.io/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/dreal/dreal4", icon = 'fa-brands fa-github'  },
+    { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker', 'Rare Events']
+developers = ['Utah State University']
+licenses = ['BSD']
+inputs = ['SMTLIB2']
+interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Barbosa2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+cvc5 is an automatic theorem prover for SMT problems.