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:
+

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2025 FM
+Copyright (c) 2025 Landon Taylor.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
 

_index.md

@@ -1,9 +1,24 @@
 +++
-title = 'Home'
-date = 2023-01-01T08:00:00-07:00
-draft = false
+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 
 +++
 
-Laborum voluptate pariatur ex culpa magna nostrud est incididunt fugiat
-pariatur do dolor ipsum enim. Consequat tempor do dolor eu. Non id id anim anim
-excepteur excepteur pariatur nostrud qui irure ullamco.
+Welcome to this collection of Formal Methods Tools, which aims to be the world'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.
+[Explore](/tools) a wide selection of tools, [contribute](/contribute) tools you make or love, and help grow the formal methods community.
+
+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="/tools">}}
+List of Tools
+{{</button>}} 
+{{<button href="/taxonomies">}}
+Taxonomy Data
+{{</button>}} 
+{{<button href="/contribute">}}
+Contribute
+{{</button>}} 
+

about.md

@@ -0,0 +1,26 @@
++++
+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. The goal of this website is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.
+
+## Key Objectives
+
+- Provide a comprehensive list of tools for formal methods.
+- Group tools by rich metadata to support collaboration and boost tools' strengths.
+- Foster a collaborative community for tool development and support.
+
+## Who's Behind This?
+
+Howdy. My name is Landon Taylor. I sometimes go by mossBiscuits. 
+This is one of my hobby projects.
+I have a passion for formal methods. When I started learning about verification, there was a sharp barrier to entry due partially to the sprawl of content online.
+I wanted to solve this problem, so I have been chipping away at this website for a while now.
+
+I love to collaborate, either on this website or on any of my other formal methods projects. Please feel free to [reach out](https://landonjtaylor.net/contact/) if you want to talk.
+
+## Get Involved
+
+I welcome contributions from anyone interested in formal methods. Add tools you love or maintain, report issues, or fix a typo. Learn more on the [Contribute](/contribute) page.

contribute.md

@@ -0,0 +1,12 @@
++++
+title = 'Contribute'
+date = 2025-06-07
++++
+
+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

@@ -0,0 +1,15 @@
++++
+title = 'MIT License'
+subtitle = 'Open-Source and Free to Use'
+date = 2025-06-07
++++
+
+MIT License
+
+Copyright (c) 2025 Landon Taylor.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

privacy.md

@@ -0,0 +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 there is no money to be made from this project.
+
+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. 
+
+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. Now go do something more interesting* :slightly_smiling_face:

taxonomies/_index.md

@@ -2,3 +2,8 @@
 title = 'All Taxonomy Data'
 layout = 'taxonomies'
 +++
+
+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).

tools/_index.md

@@ -0,0 +1,10 @@
++++
+title = "All Tools"
+layout = "section"
++++
+
+This page lists all of the 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/_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/glucose.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Glucose'
+subtitle = 'SAT Solver'
+links = [
+    { title = "Homepage", url = "https://www.labri.fr/perso/lsimon/research/glucose/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/audemard/glucose", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SAT Solver']
+developers = ['Gilles Audemard','Laurent Simon']
+licenses = ['MIT']
+inputs = ['CNF']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+<!-- {{<closed-source>}} -->
+Glucose is a SAT solver.

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

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Lingeling'
+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'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SAT Solver']
+developers = ['Johannes Kepler Universität Linz']
+licenses = ['MIT']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+<!-- {{<closed-source>}} -->
+Lingeling is a SAT solver.

tools/sat-smt/mathsat.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'MathSAT'
+subtitle = 'SMT Solver'
+links = [
+    { title = "Homepage", url = "https://mathsat.fbk.eu/", icon = 'fa-solid fa-home' },
+    # { title = "Source Code", url = "https://github.com/niklasso/minisat", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver']
+developers = ['Fondazione Bruno Kessler','DISI-University of Trento']
+licenses = ['All Rights Reserved']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+{{<closed-source>}}
+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/minisat.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'MiniSat'
+subtitle = 'SAT Solver'
+links = [
+    { title = "Homepage", url = "http://minisat.se/Main.html", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/niklasso/minisat", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SAT Solver']
+developers = ['Niklas Eén', 'Niklas Sörensson']
+licenses = ['MIT']
+# inputs = ['']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+{{<inactive year="2013">}}
+MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT. 

tools/sat-smt/opensmt.md

@@ -0,0 +1,21 @@
++++
+date = 2025-06-07
+draft = false
+title = 'OpenSMT'
+subtitle = 'SMT Solver'
+links = [
+    { title = "Homepage", url = "https://verify.inf.usi.ch/opensmt", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/usi-verification-and-security/opensmt", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SMT Solver']
+developers = ['University of Lugano']
+licenses = ['GPLv3']
+inputs = ['SMTLIB2']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['deMoura2008']
++++
+
+OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine for formal verification. OpenSMT is built on top of [MiniSAT](/tools/minisat).

tools/sat-smt/parafrost.md

@@ -0,0 +1,34 @@
++++
+date = 2025-06-07
+draft = false
+title = 'ParaFROST'
+subtitle = 'SMT Solver'
+links = [
+    # { title = "Homepage", url = "https://github.com/Z3Prover/z3", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/muhos/ParaFROST", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['SAT Solver']
+developers = ['Eindhoven University of Technology', 'Albert-Ludwigs-Universität']
+licenses = ['GPLv3']
+inputs = ['SMTLIB2']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+techniques = ['CDCL', 'GPU']
+publications = ['Osama2024']
++++
+
+ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.
+
+
+## APIs and Bindings
+This tool is available through the following interfaces:
+
+- **C API:** [Z3 C API Reference](https://z3prover.github.io/api/html/group__capi.html)
+- **C++ API:** [Z3 C++ Namespace Reference](https://z3prover.github.io/api/html/namespacez3.html)
+- **.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)
+- **Python bindings:** [z3-solver PyPI package](https://pypi.org/project/z3-solver/) ([Documentation](https://z3prover.github.io/api/html/z3.html))
+- **Rust bindings:** [z3 crate on crates.io](https://crates.io/crates/z3)
+
+

tools/sat-smt/q3b.md

@@ -0,0 +1,25 @@
++++
+date = 2025-06-07
+draft = false
+
+title = 'Q3B'
+subtitle = 'SMT Solver'
+
+links = [
+    # { title = "Homepage", url = "https://ultimate.informatik.uni-freiburg.de/smtinterpol/", icon = 'fa-solid fa-home'},
+    { title = "Source Code", url = "https://github.com/martinjonas/Q3B", icon = 'fa-brands fa-github' },
+    # { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+
+applications = ['SMT Solver']
+developers = ['Masaryk University']
+licenses = ['MIT']
+inputs = ['SMTLIB2']
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+
+publications = ['Jonas2016']
++++
+
+{{<inactive year="2023">}}
+Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.

tools/sat-smt/riss.md

@@ -0,0 +1,25 @@
++++
+date = 2025-06-07
+draft = false
+
+title = 'Riss'
+subtitle = 'SAT Tool Collection'
+
+links = [
+    # { title = "Homepage", url = "https://ultimate.informatik.uni-freiburg.de/smtinterpol/", icon = 'fa-solid fa-home'},
+    { title = "Source Code", url = "https://github.com/nmanthey/riss-solver", icon = 'fa-brands fa-github' },
+    # { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+
+applications = ['SAT Solver']
+developers = ['Norbert Manthey']
+licenses = ['LGPLv2']
+inputs = []
+interfaces = ['CLI']
+maintenance = ['Not Maintained']
+
+# publications = ['Henkel2021']
++++
+
+{{<inactive year="2017">}}
+Riss is a SAT solving tool collection.

tools/sat-smt/smt-rat.md

@@ -0,0 +1,31 @@
++++
+date = 2025-06-07
+draft = false
+
+title = 'SMT-RAT'
+subtitle = 'SMT Toolbox'
+
+links = [
+    { title = "Homepage", url = "https://ths-rwth.github.io/smtrat/", icon = 'fa-solid fa-home'},
+    { title = "Source Code", url = "https://github.com/ths-rwth/smtrat", icon = 'fa-brands fa-github' },
+    # { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+
+applications = ['SMT Solver', 'SAT Solver']
+developers = ['RWTH Aachen']
+licenses = ['MIT']
+inputs = ['SMTLIB2']
+interfaces = ['CLI', 'C++']
+maintenance = ['Actively Maintained']
+
+publications = ['Corzilius2015']
++++
+
+SMT-RAT is an SMT Real Algebra Toolbox.
+
+
+## APIs and Bindings
+This tool is available through the following interfaces:
+
+- **C++ API:** [C++ API Reference](https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25)
+

tools/sat-smt/smtinterpol.md

@@ -0,0 +1,31 @@
++++
+date = 2025-06-07
+draft = false
+
+title = 'SMTInterpol'
+subtitle = 'Interpolating SMT Solver'
+
+links = [
+    { title = "Homepage", url = "https://ultimate.informatik.uni-freiburg.de/smtinterpol/", icon = 'fa-solid fa-home'},
+    { title = "Source Code", url = "https://github.com/ultimate-pa/smtinterpol", icon = 'fa-brands fa-github' },
+    # { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+
+applications = ['SMT Solver']
+developers = ['University of Freiburg']
+licenses = ['GPLv3']
+inputs = ['SMTLIB2']
+interfaces = ['CLI', 'Java']
+maintenance = ['Actively Maintained']
+
+publications = ['Henkel2021']
++++
+
+SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
+
+
+## APIs and Bindings
+This tool is available through the following interfaces:
+
+- **Java API:** [Java API Reference](https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html)
+

tools/sat-smt/stp.md

@@ -0,0 +1,32 @@
++++
+date = 2025-06-07
+draft = false
+
+title = 'STP'
+subtitle = 'Simple Theorem Prover'
+
+links = [
+    { title = "Homepage", url = "https://stp.github.io/", icon = 'fa-solid fa-home'},
+    { title = "Source Code", url = "https://github.com/stp/stp", icon = 'fa-brands fa-github' },
+    # { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+
+applications = ['Constraint Solver', 'SMT Solver', 'Theorem Prover']
+developers = ['University of Illinois', 'Stanford University']
+licenses = ['MIT']
+inputs = ['SMTLIB2']
+interfaces = ['CLI', 'C', 'Python']
+maintenance = ['Actively Maintained']
+
+publications = ['Ganesh2007', 'Cadar2006']
++++
+
+STP is a constraint solver for quantifier-free bitvectors. 
+
+
+## APIs and Bindings
+This tool is available through the following interfaces:
+
+- **C API:** [stp C API Reference](https://stp.readthedocs.io/en/latest/#c-library-usage)
+- **Python bindings:** [stp PyPI package](https://stp.readthedocs.io/en/latest/#python-usage)
+

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/verit.md

@@ -0,0 +1,24 @@
++++
+date = 2025-06-07
+draft = false
+
+title = 'veriT'
+subtitle = 'SMT Solver'
+
+links = [
+    { title = "Homepage", url = "https://www.verit-solver.org/", icon = 'fa-solid fa-home'},
+    # { title = "Source Code", url = "https://github.com/SRI-CSL/yices2", icon = 'fa-brands fa-github' },
+    # { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+
+applications = ['SMT Solver']
+developers = ['LORIA', 'ULiege']
+licenses = ['BSD']
+inputs = ['SMTLIB2', 'DIMACS']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+
+publications = ['Schurr2021']
++++
+
+veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.

tools/sat-smt/yices.md

@@ -0,0 +1,31 @@
++++
+date = 2025-06-07
+draft = false
+
+title = 'Yices 2'
+subtitle = 'SMT Solver'
+
+links = [
+    { title = "Homepage", url = "https://yices.csl.sri.com/", icon = 'fa-solid fa-home'},
+    { title = "Source Code", url = "https://github.com/SRI-CSL/yices2", icon = 'fa-brands fa-github' },
+    # { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
+]
+
+applications = ['SMT Solver', 'SAT Solver']
+developers = ['SRI International']
+licenses = ['GPLv3']
+inputs = ['SMTLIB2', 'Yices 2']
+interfaces = ['CLI', 'Python', 'Rust']
+maintenance = ['Actively Maintained']
+
+publications = ['Dutertre2014']
++++
+
+Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.
+
+## APIs and Bindings
+This tool is available through the following interfaces:
+
+- **General API:** [Yices API Reference](https://yices.csl.sri.com/doc/index.html)
+- **Python bindings:** [yices2 PyPI package](https://pypi.org/project/yices/)
+- **Rust bindings:** [yices2 crate on crates.io](https://crates.io/crates/yices2)

tools/sat-smt/z3.md

@@ -0,0 +1,34 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Z3'
+subtitle = 'Theorem Prover'
+links = [
+    { title = "Homepage", url = "https://github.com/Z3Prover/z3", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/Z3Prover/z3", 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 = ['Microsoft Research']
+licenses = ['MIT']
+inputs = ['SMTLIB2', 'DIMACS']
+interfaces = ['CLI', 'Python', 'Rust', 'C', 'C++', 'Java', '.NET', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['deMoura2008']
++++
+
+Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
+
+
+## APIs and Bindings
+This tool is available through the following interfaces:
+
+- **C API:** [Z3 C API Reference](https://z3prover.github.io/api/html/group__capi.html)
+- **C++ API:** [Z3 C++ Namespace Reference](https://z3prover.github.io/api/html/namespacez3.html)
+- **.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)
+- **Python bindings:** [z3-solver PyPI package](https://pypi.org/project/z3-solver/) ([Documentation](https://z3prover.github.io/api/html/z3.html))
+- **Rust bindings:** [z3 crate on crates.io](https://crates.io/crates/z3)
+
+

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.

tools/yices.md

@@ -1,29 +0,0 @@
-+++
-date = 2024-02-02T04:14:54-08:00
-draft = false
-title = 'Yices 2'
-purposes = ['Verification Tools', 'Analysis Tools']
-techniques = ['Theorem Proving', 'SMT Solving', 'Model Checking']
-domains = ['Software Verification', 'Hardware Verification', 'Embedded Systems']
-languages = ['SMT-LIB', 'Yices language', 'C', 'OCaml', 'Python']
-systems = ['Discrete Systems', 'Concurrent Systems']
-interactions = ['CLI', 'C API', 'OCaml API', 'Python Bindings']
-formalisms = ['first-order logic', 'SMT-LIB', 'quantifier logic', 'bit-vectors', 'arrays', 'uninterpreted functions', 'arithmetic']
-developers = ['SRI International']
-links = [
-    { title = "Homepage", url = "https://yices.csl.sri.com/" },
-    { title = "Source Code", url = "https://github.com/SRI-CSL/yices2" },
-    { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
-]
-publications = ['Dutertre2014']
-+++
-
-Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.
-
-### Features
-
-- **SMT Solver:** Supports a wide range of theories and quantifiers.
-- **Multi-language APIs:** C, OCaml, Python, and more.
-- **Cross-platform:** Available on Windows, Linux, and macOS.
-- **Active development:** Open source and maintained by SRI International.
-

tools/z3.md

@@ -1,31 +0,0 @@
-+++
-date = 2024-02-02T04:14:54-08:00
-draft = false
-title = 'Z3'
-purposes = ['Verification Tools', 'Analysis Tools']
-techniques = ['Theorem Proving', 'SMT Solving', 'Model Checking']
-domains = ['Software Verification', 'Hardware Verification', 'Embedded Systems']
-languages = ['SMT-LIB', 'Python', 'C++', 'Java', 'C#']
-systems = ['Discrete Systems', 'Concurrent Systems']
-interactions = ['CLI', 'Python API', 'Rust Bindings', 'playground']
-formalisms = ['first-order logic', 'SMT-LIB', 'quantifier logic', 'bit-vectors', 'arrays', 'uninterpreted functions', 'arithmetic']
-developers = ['Microsoft Research']
-links = [
-    { title = "Homepage", url = "https://github.com/Z3Prover/z3" },
-    { title = "Source Code", url = "https://github.com/Z3Prover/z3" },
-    { title = "Discussions", url = "https://github.com/Z3Prover/z3/discussions" },
-    { title = "Documentation", url = "https://z3prover.github.io/api/html/" },
-    { title = "Playground", url = "https://rise4fun.com/z3" }
-]
-publications = ['deMoura2008']
-+++
-
-Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.
-
-### Features
-
-- **SMT Solver:** Supports a wide range of theories and quantifiers.
-- **Multi-language APIs:** Python, C++, Java, .NET, and more.
-- **Cross-platform:** Available on Windows, Linux, and macOS.
-- **Active development:** Open source and maintained by Microsoft Research.
-- **Web Playground:** Try Z3 online at [Rise4Fun](https://rise4fun.com/z3).