diff --git a/404.html b/404.html index 839b675..26b9a0b 100644 --- a/404.html +++ b/404.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/about/index.html b/about/index.html index 9c1ce0b..efcfa9d 100644 --- a/about/index.html +++ b/about/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/constraint-solver/index.html b/applications/constraint-solver/index.html index b124272..0209612 100644 --- a/applications/constraint-solver/index.html +++ b/applications/constraint-solver/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/constraint-solver/index.xml b/applications/constraint-solver/index.xml index e264b7e..a48a8ed 100644 --- a/applications/constraint-solver/index.xml +++ b/applications/constraint-solver/index.xml @@ -2,17 +2,17 @@ Constraint Solver on Formal Methods Tools - https://example.org/applications/constraint-solver/ + https://fmtools.fyi/applications/constraint-solver/ Recent content in Constraint Solver on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> diff --git a/applications/index.html b/applications/index.html index 70963da..eab6500 100644 --- a/applications/index.html +++ b/applications/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/index.xml b/applications/index.xml index d08929c..184069a 100644 --- a/applications/index.xml +++ b/applications/index.xml @@ -2,52 +2,52 @@ Applications on Formal Methods Tools - https://example.org/applications/ + https://fmtools.fyi/applications/ Recent content in Applications on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Constraint Solver - https://example.org/applications/constraint-solver/ + https://fmtools.fyi/applications/constraint-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/constraint-solver/ + https://fmtools.fyi/applications/constraint-solver/ Model Checker - https://example.org/applications/model-checker/ + https://fmtools.fyi/applications/model-checker/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/model-checker/ + https://fmtools.fyi/applications/model-checker/ Probabilistic Model Checker - https://example.org/applications/probabilistic-model-checker/ + https://fmtools.fyi/applications/probabilistic-model-checker/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/probabilistic-model-checker/ + https://fmtools.fyi/applications/probabilistic-model-checker/ SAT Solver - https://example.org/applications/sat-solver/ + https://fmtools.fyi/applications/sat-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/sat-solver/ + https://fmtools.fyi/applications/sat-solver/ SMT Solver - https://example.org/applications/smt-solver/ + https://fmtools.fyi/applications/smt-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/smt-solver/ + https://fmtools.fyi/applications/smt-solver/ Theorem Prover - https://example.org/applications/theorem-prover/ + https://fmtools.fyi/applications/theorem-prover/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/theorem-prover/ + https://fmtools.fyi/applications/theorem-prover/ diff --git a/applications/model-checker/index.html b/applications/model-checker/index.html index 59b5815..24f5c64 100644 --- a/applications/model-checker/index.html +++ b/applications/model-checker/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/model-checker/index.xml b/applications/model-checker/index.xml index 6edf740..ca31603 100644 --- a/applications/model-checker/index.xml +++ b/applications/model-checker/index.xml @@ -2,17 +2,17 @@ Model Checker on Formal Methods Tools - https://example.org/applications/model-checker/ + https://fmtools.fyi/applications/model-checker/ Recent content in Model Checker on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> diff --git a/applications/probabilistic-model-checker/index.html b/applications/probabilistic-model-checker/index.html index b5a1ebc..b29cf88 100644 --- a/applications/probabilistic-model-checker/index.html +++ b/applications/probabilistic-model-checker/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/probabilistic-model-checker/index.xml b/applications/probabilistic-model-checker/index.xml index 22dd233..9372700 100644 --- a/applications/probabilistic-model-checker/index.xml +++ b/applications/probabilistic-model-checker/index.xml @@ -2,31 +2,31 @@ Probabilistic Model Checker on Formal Methods Tools - https://example.org/applications/probabilistic-model-checker/ + https://fmtools.fyi/applications/probabilistic-model-checker/ Recent content in Probabilistic Model Checker on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/applications/sat-solver/index.html b/applications/sat-solver/index.html index b472579..9951e74 100644 --- a/applications/sat-solver/index.html +++ b/applications/sat-solver/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/sat-solver/index.xml b/applications/sat-solver/index.xml index ebad5fd..0b0737b 100644 --- a/applications/sat-solver/index.xml +++ b/applications/sat-solver/index.xml @@ -2,87 +2,87 @@ SAT Solver on Formal Methods Tools - https://example.org/applications/sat-solver/ + https://fmtools.fyi/applications/sat-solver/ Recent content in SAT Solver on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> Riss - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/applications/smt-solver/index.html b/applications/smt-solver/index.html index 0eaf7b9..dd0d764 100644 --- a/applications/smt-solver/index.html +++ b/applications/smt-solver/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/smt-solver/index.xml b/applications/smt-solver/index.xml index cdb1ba0..6641d56 100644 --- a/applications/smt-solver/index.xml +++ b/applications/smt-solver/index.xml @@ -2,115 +2,115 @@ SMT Solver on Formal Methods Tools - https://example.org/applications/smt-solver/ + https://fmtools.fyi/applications/smt-solver/ Recent content in SMT Solver on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> 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.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/applications/theorem-prover/index.html b/applications/theorem-prover/index.html index b235221..e05b67a 100644 --- a/applications/theorem-prover/index.html +++ b/applications/theorem-prover/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/theorem-prover/index.xml b/applications/theorem-prover/index.xml index d015967..db8b5cd 100644 --- a/applications/theorem-prover/index.xml +++ b/applications/theorem-prover/index.xml @@ -2,52 +2,52 @@ Theorem Prover on Formal Methods Tools - https://example.org/applications/theorem-prover/ + https://fmtools.fyi/applications/theorem-prover/ Recent content in Theorem Prover on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/contribute/index.html b/contribute/index.html index a656358..0ccb0c9 100644 --- a/contribute/index.html +++ b/contribute/index.html @@ -17,16 +17,16 @@ Quick Links Request addding a tool: Submit"> - + - + - - - - + + + + - + diff --git a/developers/albert-ludwigs-universität/index.html b/developers/albert-ludwigs-universität/index.html index e0eb14a..bc16fe1 100644 --- a/developers/albert-ludwigs-universität/index.html +++ b/developers/albert-ludwigs-universität/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/albert-ludwigs-universität/index.xml b/developers/albert-ludwigs-universität/index.xml index 96446f6..c229a26 100644 --- a/developers/albert-ludwigs-universität/index.xml +++ b/developers/albert-ludwigs-universität/index.xml @@ -2,17 +2,17 @@ Albert-Ludwigs-Universität on Formal Methods Tools - https://example.org/developers/albert-ludwigs-universit%C3%A4t/ + https://fmtools.fyi/developers/albert-ludwigs-universit%C3%A4t/ Recent content in Albert-Ludwigs-Universität on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/developers/cea/index.html b/developers/cea/index.html index 131244a..7885986 100644 --- a/developers/cea/index.html +++ b/developers/cea/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/cea/index.xml b/developers/cea/index.xml index 06e663b..f2135e6 100644 --- a/developers/cea/index.xml +++ b/developers/cea/index.xml @@ -2,17 +2,17 @@ CEA on Formal Methods Tools - https://example.org/developers/cea/ + https://fmtools.fyi/developers/cea/ Recent content in CEA on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> diff --git a/developers/disi-university-of-trento/index.html b/developers/disi-university-of-trento/index.html index 0ae9017..1b79d46 100644 --- a/developers/disi-university-of-trento/index.html +++ b/developers/disi-university-of-trento/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/disi-university-of-trento/index.xml b/developers/disi-university-of-trento/index.xml index 05790f9..af3b052 100644 --- a/developers/disi-university-of-trento/index.xml +++ b/developers/disi-university-of-trento/index.xml @@ -2,17 +2,17 @@ DISI-University of Trento on Formal Methods Tools - https://example.org/developers/disi-university-of-trento/ + https://fmtools.fyi/developers/disi-university-of-trento/ Recent content in DISI-University of Trento on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> diff --git a/developers/eindhoven-university-of-technology/index.html b/developers/eindhoven-university-of-technology/index.html index 2bba910..298e303 100644 --- a/developers/eindhoven-university-of-technology/index.html +++ b/developers/eindhoven-university-of-technology/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/eindhoven-university-of-technology/index.xml b/developers/eindhoven-university-of-technology/index.xml index 48a871d..6f3262c 100644 --- a/developers/eindhoven-university-of-technology/index.xml +++ b/developers/eindhoven-university-of-technology/index.xml @@ -2,17 +2,17 @@ Eindhoven University of Technology on Formal Methods Tools - https://example.org/developers/eindhoven-university-of-technology/ + https://fmtools.fyi/developers/eindhoven-university-of-technology/ Recent content in Eindhoven University of Technology on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/developers/fondazione-bruno-kessler/index.html b/developers/fondazione-bruno-kessler/index.html index 9fdd8a8..3283a70 100644 --- a/developers/fondazione-bruno-kessler/index.html +++ b/developers/fondazione-bruno-kessler/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/fondazione-bruno-kessler/index.xml b/developers/fondazione-bruno-kessler/index.xml index c7231af..8387927 100644 --- a/developers/fondazione-bruno-kessler/index.xml +++ b/developers/fondazione-bruno-kessler/index.xml @@ -2,17 +2,17 @@ Fondazione Bruno Kessler on Formal Methods Tools - https://example.org/developers/fondazione-bruno-kessler/ + https://fmtools.fyi/developers/fondazione-bruno-kessler/ Recent content in Fondazione Bruno Kessler on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> diff --git a/developers/gilles-audemard/index.html b/developers/gilles-audemard/index.html index 9824986..200dcf3 100644 --- a/developers/gilles-audemard/index.html +++ b/developers/gilles-audemard/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/gilles-audemard/index.xml b/developers/gilles-audemard/index.xml index 3c9b927..68cce14 100644 --- a/developers/gilles-audemard/index.xml +++ b/developers/gilles-audemard/index.xml @@ -2,17 +2,17 @@ Gilles Audemard on Formal Methods Tools - https://example.org/developers/gilles-audemard/ + https://fmtools.fyi/developers/gilles-audemard/ Recent content in Gilles Audemard on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/developers/index.html b/developers/index.html index e47a024..2f0c1fe 100644 --- a/developers/index.html +++ b/developers/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/index.xml b/developers/index.xml index 0ddccb1..f612dcd 100644 --- a/developers/index.xml +++ b/developers/index.xml @@ -2,192 +2,192 @@ Developers on Formal Methods Tools - https://example.org/developers/ + https://fmtools.fyi/developers/ Recent content in Developers on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Albert-Ludwigs-Universität - https://example.org/developers/albert-ludwigs-universit%C3%A4t/ + https://fmtools.fyi/developers/albert-ludwigs-universit%C3%A4t/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/albert-ludwigs-universit%C3%A4t/ + https://fmtools.fyi/developers/albert-ludwigs-universit%C3%A4t/ CEA - https://example.org/developers/cea/ + https://fmtools.fyi/developers/cea/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/cea/ + https://fmtools.fyi/developers/cea/ DISI-University of Trento - https://example.org/developers/disi-university-of-trento/ + https://fmtools.fyi/developers/disi-university-of-trento/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/disi-university-of-trento/ + https://fmtools.fyi/developers/disi-university-of-trento/ Eindhoven University of Technology - https://example.org/developers/eindhoven-university-of-technology/ + https://fmtools.fyi/developers/eindhoven-university-of-technology/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/eindhoven-university-of-technology/ + https://fmtools.fyi/developers/eindhoven-university-of-technology/ Fondazione Bruno Kessler - https://example.org/developers/fondazione-bruno-kessler/ + https://fmtools.fyi/developers/fondazione-bruno-kessler/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/fondazione-bruno-kessler/ + https://fmtools.fyi/developers/fondazione-bruno-kessler/ Gilles Audemard - https://example.org/developers/gilles-audemard/ + https://fmtools.fyi/developers/gilles-audemard/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/gilles-audemard/ + https://fmtools.fyi/developers/gilles-audemard/ INRIA Rhône-Alpes - https://example.org/developers/inria-rh%C3%B4ne-alpes/ + https://fmtools.fyi/developers/inria-rh%C3%B4ne-alpes/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/inria-rh%C3%B4ne-alpes/ + https://fmtools.fyi/developers/inria-rh%C3%B4ne-alpes/ Johannes Kepler Universität Linz - https://example.org/developers/johannes-kepler-universit%C3%A4t-linz/ + https://fmtools.fyi/developers/johannes-kepler-universit%C3%A4t-linz/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/johannes-kepler-universit%C3%A4t-linz/ + https://fmtools.fyi/developers/johannes-kepler-universit%C3%A4t-linz/ Laurent Simon - https://example.org/developers/laurent-simon/ + https://fmtools.fyi/developers/laurent-simon/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/laurent-simon/ + https://fmtools.fyi/developers/laurent-simon/ LORIA - https://example.org/developers/loria/ + https://fmtools.fyi/developers/loria/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/loria/ + https://fmtools.fyi/developers/loria/ Masaryk University - https://example.org/developers/masaryk-university/ + https://fmtools.fyi/developers/masaryk-university/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/masaryk-university/ + https://fmtools.fyi/developers/masaryk-university/ Microsoft Research - https://example.org/developers/microsoft-research/ + https://fmtools.fyi/developers/microsoft-research/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/microsoft-research/ + https://fmtools.fyi/developers/microsoft-research/ Niklas Eén - https://example.org/developers/niklas-e%C3%A9n/ + https://fmtools.fyi/developers/niklas-e%C3%A9n/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/niklas-e%C3%A9n/ + https://fmtools.fyi/developers/niklas-e%C3%A9n/ Niklas Sörensson - https://example.org/developers/niklas-s%C3%B6rensson/ + https://fmtools.fyi/developers/niklas-s%C3%B6rensson/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/niklas-s%C3%B6rensson/ + https://fmtools.fyi/developers/niklas-s%C3%B6rensson/ Norbert Manthey - https://example.org/developers/norbert-manthey/ + https://fmtools.fyi/developers/norbert-manthey/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/norbert-manthey/ + https://fmtools.fyi/developers/norbert-manthey/ Oxford University - https://example.org/developers/oxford-university/ + https://fmtools.fyi/developers/oxford-university/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/oxford-university/ + https://fmtools.fyi/developers/oxford-university/ RWTH Aachen - https://example.org/developers/rwth-aachen/ + https://fmtools.fyi/developers/rwth-aachen/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/rwth-aachen/ + https://fmtools.fyi/developers/rwth-aachen/ SRI International - https://example.org/developers/sri-international/ + https://fmtools.fyi/developers/sri-international/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/sri-international/ + https://fmtools.fyi/developers/sri-international/ Stanford University - https://example.org/developers/stanford-university/ + https://fmtools.fyi/developers/stanford-university/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/stanford-university/ + https://fmtools.fyi/developers/stanford-university/ ULiege - https://example.org/developers/uliege/ + https://fmtools.fyi/developers/uliege/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/uliege/ + https://fmtools.fyi/developers/uliege/ University of Freiburg - https://example.org/developers/university-of-freiburg/ + https://fmtools.fyi/developers/university-of-freiburg/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-freiburg/ + https://fmtools.fyi/developers/university-of-freiburg/ University of Illinois - https://example.org/developers/university-of-illinois/ + https://fmtools.fyi/developers/university-of-illinois/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-illinois/ + https://fmtools.fyi/developers/university-of-illinois/ University of Iowa - https://example.org/developers/university-of-iowa/ + https://fmtools.fyi/developers/university-of-iowa/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-iowa/ + https://fmtools.fyi/developers/university-of-iowa/ University of Lugano - https://example.org/developers/university-of-lugano/ + https://fmtools.fyi/developers/university-of-lugano/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-lugano/ + https://fmtools.fyi/developers/university-of-lugano/ University of Virginia - https://example.org/developers/university-of-virginia/ + https://fmtools.fyi/developers/university-of-virginia/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-virginia/ + https://fmtools.fyi/developers/university-of-virginia/ Utah State University - https://example.org/developers/utah-state-university/ + https://fmtools.fyi/developers/utah-state-university/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/utah-state-university/ + https://fmtools.fyi/developers/utah-state-university/ diff --git a/developers/inria-rhône-alpes/index.html b/developers/inria-rhône-alpes/index.html index f203eb3..46a1afa 100644 --- a/developers/inria-rhône-alpes/index.html +++ b/developers/inria-rhône-alpes/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/inria-rhône-alpes/index.xml b/developers/inria-rhône-alpes/index.xml index ad6533f..3df2ac7 100644 --- a/developers/inria-rhône-alpes/index.xml +++ b/developers/inria-rhône-alpes/index.xml @@ -2,17 +2,17 @@ INRIA Rhône-Alpes on Formal Methods Tools - https://example.org/developers/inria-rh%C3%B4ne-alpes/ + https://fmtools.fyi/developers/inria-rh%C3%B4ne-alpes/ Recent content in INRIA Rhône-Alpes on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> diff --git a/developers/johannes-kepler-universität-linz/index.html b/developers/johannes-kepler-universität-linz/index.html index 2929daa..154a755 100644 --- a/developers/johannes-kepler-universität-linz/index.html +++ b/developers/johannes-kepler-universität-linz/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/johannes-kepler-universität-linz/index.xml b/developers/johannes-kepler-universität-linz/index.xml index 85d9f15..ba16288 100644 --- a/developers/johannes-kepler-universität-linz/index.xml +++ b/developers/johannes-kepler-universität-linz/index.xml @@ -2,24 +2,24 @@ Johannes Kepler Universität Linz on Formal Methods Tools - https://example.org/developers/johannes-kepler-universit%C3%A4t-linz/ + https://fmtools.fyi/developers/johannes-kepler-universit%C3%A4t-linz/ Recent content in Johannes Kepler Universität Linz on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> diff --git a/developers/laurent-simon/index.html b/developers/laurent-simon/index.html index 405be5f..b0999a5 100644 --- a/developers/laurent-simon/index.html +++ b/developers/laurent-simon/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/laurent-simon/index.xml b/developers/laurent-simon/index.xml index f9314b9..d710d39 100644 --- a/developers/laurent-simon/index.xml +++ b/developers/laurent-simon/index.xml @@ -2,17 +2,17 @@ Laurent Simon on Formal Methods Tools - https://example.org/developers/laurent-simon/ + https://fmtools.fyi/developers/laurent-simon/ Recent content in Laurent Simon on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/developers/loria/index.html b/developers/loria/index.html index a69b196..baa9a17 100644 --- a/developers/loria/index.html +++ b/developers/loria/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/loria/index.xml b/developers/loria/index.xml index 8aa6973..3374759 100644 --- a/developers/loria/index.xml +++ b/developers/loria/index.xml @@ -2,17 +2,17 @@ LORIA on Formal Methods Tools - https://example.org/developers/loria/ + https://fmtools.fyi/developers/loria/ Recent content in LORIA on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> diff --git a/developers/masaryk-university/index.html b/developers/masaryk-university/index.html index bf5f235..22fe401 100644 --- a/developers/masaryk-university/index.html +++ b/developers/masaryk-university/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/masaryk-university/index.xml b/developers/masaryk-university/index.xml index 2f36b3b..2bcf2ad 100644 --- a/developers/masaryk-university/index.xml +++ b/developers/masaryk-university/index.xml @@ -2,17 +2,17 @@ Masaryk University on Formal Methods Tools - https://example.org/developers/masaryk-university/ + https://fmtools.fyi/developers/masaryk-university/ Recent content in Masaryk University on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> diff --git a/developers/microsoft-research/index.html b/developers/microsoft-research/index.html index de77307..1aa19e9 100644 --- a/developers/microsoft-research/index.html +++ b/developers/microsoft-research/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/microsoft-research/index.xml b/developers/microsoft-research/index.xml index 185f3df..b92b57d 100644 --- a/developers/microsoft-research/index.xml +++ b/developers/microsoft-research/index.xml @@ -2,17 +2,17 @@ Microsoft Research on Formal Methods Tools - https://example.org/developers/microsoft-research/ + https://fmtools.fyi/developers/microsoft-research/ Recent content in Microsoft Research on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/developers/niklas-eén/index.html b/developers/niklas-eén/index.html index 4060a5d..66fbe91 100644 --- a/developers/niklas-eén/index.html +++ b/developers/niklas-eén/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/niklas-eén/index.xml b/developers/niklas-eén/index.xml index 8cfe3df..d42a58e 100644 --- a/developers/niklas-eén/index.xml +++ b/developers/niklas-eén/index.xml @@ -2,17 +2,17 @@ Niklas Eén on Formal Methods Tools - https://example.org/developers/niklas-e%C3%A9n/ + https://fmtools.fyi/developers/niklas-e%C3%A9n/ Recent content in Niklas Eén on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> diff --git a/developers/niklas-sörensson/index.html b/developers/niklas-sörensson/index.html index 2f66500..098e457 100644 --- a/developers/niklas-sörensson/index.html +++ b/developers/niklas-sörensson/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/niklas-sörensson/index.xml b/developers/niklas-sörensson/index.xml index e387246..0e82313 100644 --- a/developers/niklas-sörensson/index.xml +++ b/developers/niklas-sörensson/index.xml @@ -2,17 +2,17 @@ Niklas Sörensson on Formal Methods Tools - https://example.org/developers/niklas-s%C3%B6rensson/ + https://fmtools.fyi/developers/niklas-s%C3%B6rensson/ Recent content in Niklas Sörensson on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> diff --git a/developers/norbert-manthey/index.html b/developers/norbert-manthey/index.html index eb30520..44b1aec 100644 --- a/developers/norbert-manthey/index.html +++ b/developers/norbert-manthey/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/norbert-manthey/index.xml b/developers/norbert-manthey/index.xml index ab73409..9f4daca 100644 --- a/developers/norbert-manthey/index.xml +++ b/developers/norbert-manthey/index.xml @@ -2,17 +2,17 @@ Norbert Manthey on Formal Methods Tools - https://example.org/developers/norbert-manthey/ + https://fmtools.fyi/developers/norbert-manthey/ Recent content in Norbert Manthey on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Riss - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> diff --git a/developers/oxford-university/index.html b/developers/oxford-university/index.html index 0457f91..f3300b5 100644 --- a/developers/oxford-university/index.html +++ b/developers/oxford-university/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/oxford-university/index.xml b/developers/oxford-university/index.xml index 0dd71c0..58317d6 100644 --- a/developers/oxford-university/index.xml +++ b/developers/oxford-university/index.xml @@ -2,17 +2,17 @@ Oxford University on Formal Methods Tools - https://example.org/developers/oxford-university/ + https://fmtools.fyi/developers/oxford-university/ Recent content in Oxford University on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> diff --git a/developers/rwth-aachen/index.html b/developers/rwth-aachen/index.html index e43ee24..7d6002f 100644 --- a/developers/rwth-aachen/index.html +++ b/developers/rwth-aachen/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/rwth-aachen/index.xml b/developers/rwth-aachen/index.xml index 78de16f..537f72e 100644 --- a/developers/rwth-aachen/index.xml +++ b/developers/rwth-aachen/index.xml @@ -2,24 +2,24 @@ RWTH Aachen on Formal Methods Tools - https://example.org/developers/rwth-aachen/ + https://fmtools.fyi/developers/rwth-aachen/ Recent content in RWTH Aachen on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/developers/sri-international/index.html b/developers/sri-international/index.html index 938e783..2c55974 100644 --- a/developers/sri-international/index.html +++ b/developers/sri-international/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/sri-international/index.xml b/developers/sri-international/index.xml index e4ec35f..32a22d9 100644 --- a/developers/sri-international/index.xml +++ b/developers/sri-international/index.xml @@ -2,24 +2,24 @@ SRI International on Formal Methods Tools - https://example.org/developers/sri-international/ + https://fmtools.fyi/developers/sri-international/ Recent content in SRI International on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> diff --git a/developers/stanford-university/index.html b/developers/stanford-university/index.html index 1767303..6a53260 100644 --- a/developers/stanford-university/index.html +++ b/developers/stanford-university/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/stanford-university/index.xml b/developers/stanford-university/index.xml index 39b5df4..154dcc0 100644 --- a/developers/stanford-university/index.xml +++ b/developers/stanford-university/index.xml @@ -2,45 +2,45 @@ Stanford University on Formal Methods Tools - https://example.org/developers/stanford-university/ + https://fmtools.fyi/developers/stanford-university/ Recent content in Stanford University on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> diff --git a/developers/uliege/index.html b/developers/uliege/index.html index c4c6dab..f5b41c8 100644 --- a/developers/uliege/index.html +++ b/developers/uliege/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/uliege/index.xml b/developers/uliege/index.xml index cd3ac19..c23c93f 100644 --- a/developers/uliege/index.xml +++ b/developers/uliege/index.xml @@ -2,17 +2,17 @@ ULiege on Formal Methods Tools - https://example.org/developers/uliege/ + https://fmtools.fyi/developers/uliege/ Recent content in ULiege on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> diff --git a/developers/university-of-freiburg/index.html b/developers/university-of-freiburg/index.html index 7f29691..95383ea 100644 --- a/developers/university-of-freiburg/index.html +++ b/developers/university-of-freiburg/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-freiburg/index.xml b/developers/university-of-freiburg/index.xml index 8e4db55..1c40725 100644 --- a/developers/university-of-freiburg/index.xml +++ b/developers/university-of-freiburg/index.xml @@ -2,17 +2,17 @@ University of Freiburg on Formal Methods Tools - https://example.org/developers/university-of-freiburg/ + https://fmtools.fyi/developers/university-of-freiburg/ Recent content in University of Freiburg on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> diff --git a/developers/university-of-illinois/index.html b/developers/university-of-illinois/index.html index 123d5b0..89d1e66 100644 --- a/developers/university-of-illinois/index.html +++ b/developers/university-of-illinois/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-illinois/index.xml b/developers/university-of-illinois/index.xml index 54d16f7..a08e3ba 100644 --- a/developers/university-of-illinois/index.xml +++ b/developers/university-of-illinois/index.xml @@ -2,17 +2,17 @@ University of Illinois on Formal Methods Tools - https://example.org/developers/university-of-illinois/ + https://fmtools.fyi/developers/university-of-illinois/ Recent content in University of Illinois on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> diff --git a/developers/university-of-iowa/index.html b/developers/university-of-iowa/index.html index 6b1eec8..8785612 100644 --- a/developers/university-of-iowa/index.html +++ b/developers/university-of-iowa/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-iowa/index.xml b/developers/university-of-iowa/index.xml index f80565b..f78e1b5 100644 --- a/developers/university-of-iowa/index.xml +++ b/developers/university-of-iowa/index.xml @@ -2,24 +2,24 @@ University of Iowa on Formal Methods Tools - https://example.org/developers/university-of-iowa/ + https://fmtools.fyi/developers/university-of-iowa/ Recent content in University of Iowa on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> diff --git a/developers/university-of-lugano/index.html b/developers/university-of-lugano/index.html index 0201311..fe442b9 100644 --- a/developers/university-of-lugano/index.html +++ b/developers/university-of-lugano/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-lugano/index.xml b/developers/university-of-lugano/index.xml index a2af1a1..f69df88 100644 --- a/developers/university-of-lugano/index.xml +++ b/developers/university-of-lugano/index.xml @@ -2,18 +2,18 @@ University of Lugano on Formal Methods Tools - https://example.org/developers/university-of-lugano/ + https://fmtools.fyi/developers/university-of-lugano/ Recent content in University of Lugano on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> diff --git a/developers/university-of-virginia/index.html b/developers/university-of-virginia/index.html index 3abd5d9..e666ef2 100644 --- a/developers/university-of-virginia/index.html +++ b/developers/university-of-virginia/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-virginia/index.xml b/developers/university-of-virginia/index.xml index 3778902..ecaa995 100644 --- a/developers/university-of-virginia/index.xml +++ b/developers/university-of-virginia/index.xml @@ -2,17 +2,17 @@ University of Virginia on Formal Methods Tools - https://example.org/developers/university-of-virginia/ + https://fmtools.fyi/developers/university-of-virginia/ Recent content in University of Virginia on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> diff --git a/developers/utah-state-university/index.html b/developers/utah-state-university/index.html index 72c042d..019b984 100644 --- a/developers/utah-state-university/index.html +++ b/developers/utah-state-university/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/utah-state-university/index.xml b/developers/utah-state-university/index.xml index 67a0e82..cf6c3e0 100644 --- a/developers/utah-state-university/index.xml +++ b/developers/utah-state-university/index.xml @@ -2,17 +2,17 @@ Utah State University on Formal Methods Tools - https://example.org/developers/utah-state-university/ + https://fmtools.fyi/developers/utah-state-university/ Recent content in Utah State University on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> diff --git a/domains/index.html b/domains/index.html index 89fdf01..4fdf1ec 100644 --- a/domains/index.html +++ b/domains/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/domains/index.xml b/domains/index.xml index b960c67..bcb430a 100644 --- a/domains/index.xml +++ b/domains/index.xml @@ -2,10 +2,10 @@ Domains on Formal Methods Tools - https://example.org/domains/ + https://fmtools.fyi/domains/ Recent content in Domains on Formal Methods Tools Hugo en-us - + diff --git a/index.html b/index.html index c332665..b34dfb4 100644 --- a/index.html +++ b/index.html @@ -15,16 +15,16 @@ - + - + - - - - + + + + - + @@ -101,41 +101,6 @@ Contribute

Try Something New

This list shows a selection of 20 random tools, refreshed every time this site is updated.

-
-

- veriT - - SMT Solver - -

-

veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal …

- veriT -
- -
-

- Yices 2 - - SMT Solver - -

-

Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas …

- Yices 2 -
- -
-

- SMT-RAT - - SMT Toolbox - -

-

SMT-RAT is an SMT Real Algebra Toolbox. -APIs and Bindings This tool is available through the following interfaces: -C++ API: …

- SMT-RAT -
-

Glucose @@ -148,133 +113,6 @@ C++ API: …

Glucose

-
-

- Colibri - - SMT Solver - -

-

Colibri is an SMT solver. -

- Colibri -
- -
-

- Riss - - SAT Tool Collection - -

-

[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. -

- Riss -
- -
-

- STAMINA - - Probabilistic Model Checker - -

-

A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either Storm or PRISM. …

- STAMINA -
- -
-

- ParaFROST - - SMT Solver - -

-

ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in …

- ParaFROST -
- -
-

- MiniSat - - SAT Solver - -

-

[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and …

- MiniSat -
- -
-

- OpenSMT - - SMT Solver - -

-

OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand …

- OpenSMT -
- -
-

- Z3 - - Theorem Prover - -

-

Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. -APIs and Bindings This tool is available …

- Z3 -
- -
-

- Q3B - - SMT Solver - -

-

[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs. -

- Q3B -
- -
-

- STP - - Simple Theorem Prover - -

-

STP is a constraint solver for quantifier-free bitvectors. -APIs and Bindings This tool is available through the following …

- STP -
- -
-

- cvc4 - - Theorem Prover - -

-

[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5 -

- cvc4 -
- -
-

- MathSAT - - SMT Solver - -

-

[ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers …

- MathSAT -
-

CryptoMiniSat @@ -290,25 +128,50 @@ C++ Namespace: …

- cvc5 - - Theorem Prover - -

-

cvc5 is an automatic theorem prover for SMT problems. -

- cvc5 -
- -
-

- Boolector + Colibri SMT Solver

-

[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …

- Boolector +

Colibri is an SMT solver. +

+ Colibri +
+ +
+

+ SMT-RAT + + SMT Toolbox + +

+

SMT-RAT is an SMT Real Algebra Toolbox. +APIs and Bindings This tool is available through the following interfaces: +C++ API: …

+ SMT-RAT +
+ +
+

+ PRISM + + Probabilistic Model Checker + +

+

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or …

+ PRISM +
+ +
+

+ Sally + + Probabilistic Model Checker + +

+

Sally is a model checker for infinite state systems described as transition systems. +

+ Sally
@@ -325,13 +188,151 @@ APIs and Bindings This tool is …

- PRISM + MiniSat + + SAT Solver + +

+

[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and …

+ MiniSat +
+ +
+

+ cvc5 + + Theorem Prover + +

+

cvc5 is an automatic theorem prover for SMT problems. +

+ cvc5 +
+ +
+

+ Z3 + + Theorem Prover + +

+

Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. +APIs and Bindings This tool is available …

+ Z3 +
+ +
+

+ Riss + + SAT Tool Collection + +

+

[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. +

+ Riss +
+ +
+

+ Boolector + + SMT Solver + +

+

[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …

+ Boolector +
+ +
+

+ cvc4 + + Theorem Prover + +

+

[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5 +

+ cvc4 +
+ +
+

+ Bitwuzla + + SMT Solver + +

+

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point …

+ Bitwuzla +
+ +
+

+ ParaFROST + + SMT Solver + +

+

ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in …

+ ParaFROST +
+ +
+

+ STAMINA Probabilistic Model Checker

-

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or …

- PRISM +

A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either Storm or PRISM. …

+ STAMINA +
+ +
+

+ Yices 2 + + SMT Solver + +

+

Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas …

+ Yices 2 +
+ +
+

+ STP + + Simple Theorem Prover + +

+

STP is a constraint solver for quantifier-free bitvectors. +APIs and Bindings This tool is available through the following …

+ STP +
+ +
+

+ Lingeling + + SAT Solver + +

+

Lingeling is a SAT solver. +

+ Lingeling +
+ +
+

+ veriT + + SMT Solver + +

+

veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal …

+ veriT
diff --git a/index.xml b/index.xml index 40b4b16..08913ca 100644 --- a/index.xml +++ b/index.xml @@ -2,213 +2,213 @@ The Ultimate Formal Methods Toolbox on Formal Methods Tools - https://example.org/ + https://fmtools.fyi/ Recent content in The Ultimate Formal Methods Toolbox on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> 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.</p> Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> Riss - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> About - https://example.org/about/ + https://fmtools.fyi/about/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/about/ + https://fmtools.fyi/about/ <p>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.</p> <h2 id="key-objectives">Key Objectives</h2> <ul> <li>Provide a comprehensive list of tools for formal methods.</li> <li>Group tools by rich metadata to support collaboration and boost tools&rsquo; strengths.</li> <li>Foster a collaborative community for tool development and support.</li> </ul> <h2 id="whos-behind-this">Who&rsquo;s Behind This?</h2> <p>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.</p> Contribute - https://example.org/contribute/ + https://fmtools.fyi/contribute/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/contribute/ + https://fmtools.fyi/contribute/ <p>Instructions coming soon. Please see <a href="https://gitmoss.fyi/fmtools/content/wiki/Contribute" target="_blank" >https://gitmoss.fyi/fmtools/content/wiki/Contribute</a> for temporary instructions.</p> <h2 id="quick-links">Quick Links</h2> <ul> <li>Request addding a tool: <a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2fadd_tool.md" target="_blank" >Submit Git Issue</a></li> <li>Request fixing a tool: <a href="https://gitmoss.fyi/fmtools/content/issues/new?template=.gitea%2fissue_template%2ffix_tool.md" target="_blank" >Submit Git Issue</a></li> </ul> MIT License - https://example.org/license/ + https://fmtools.fyi/license/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/license/ + https://fmtools.fyi/license/ <p>MIT License</p> <p>Copyright (c) 2025 Landon Taylor.</p> <p>Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the &ldquo;Software&rdquo;), 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:</p> Privacy - https://example.org/privacy/ + https://fmtools.fyi/privacy/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/privacy/ + https://fmtools.fyi/privacy/ <p>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.</p> <p>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&rsquo;s content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website&rsquo;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.</p> diff --git a/inputs/cnf/index.html b/inputs/cnf/index.html index bb18d37..f53ea99 100644 --- a/inputs/cnf/index.html +++ b/inputs/cnf/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/cnf/index.xml b/inputs/cnf/index.xml index 705f38f..926ba00 100644 --- a/inputs/cnf/index.xml +++ b/inputs/cnf/index.xml @@ -2,24 +2,24 @@ CNF on Formal Methods Tools - https://example.org/inputs/cnf/ + https://fmtools.fyi/inputs/cnf/ Recent content in CNF on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/inputs/dimacs/index.html b/inputs/dimacs/index.html index 121be04..14ad140 100644 --- a/inputs/dimacs/index.html +++ b/inputs/dimacs/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/dimacs/index.xml b/inputs/dimacs/index.xml index 1df53ce..620be49 100644 --- a/inputs/dimacs/index.xml +++ b/inputs/dimacs/index.xml @@ -2,24 +2,24 @@ DIMACS on Formal Methods Tools - https://example.org/inputs/dimacs/ + https://fmtools.fyi/inputs/dimacs/ Recent content in DIMACS on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/inputs/galileo/index.html b/inputs/galileo/index.html index 230a64d..fed65ea 100644 --- a/inputs/galileo/index.html +++ b/inputs/galileo/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/galileo/index.xml b/inputs/galileo/index.xml index 583e365..8dd7d8b 100644 --- a/inputs/galileo/index.xml +++ b/inputs/galileo/index.xml @@ -2,17 +2,17 @@ Galileo on Formal Methods Tools - https://example.org/inputs/galileo/ + https://fmtools.fyi/inputs/galileo/ Recent content in Galileo on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/inputs/greatspn/index.html b/inputs/greatspn/index.html index 5f0f4f5..b0bdefb 100644 --- a/inputs/greatspn/index.html +++ b/inputs/greatspn/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/greatspn/index.xml b/inputs/greatspn/index.xml index 7d52a60..327c39c 100644 --- a/inputs/greatspn/index.xml +++ b/inputs/greatspn/index.xml @@ -2,17 +2,17 @@ GreatSPN on Formal Methods Tools - https://example.org/inputs/greatspn/ + https://fmtools.fyi/inputs/greatspn/ Recent content in GreatSPN on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/inputs/index.html b/inputs/index.html index 4106095..475a06e 100644 --- a/inputs/index.html +++ b/inputs/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/index.xml b/inputs/index.xml index d5b0723..579016f 100644 --- a/inputs/index.xml +++ b/inputs/index.xml @@ -2,87 +2,87 @@ Inputs on Formal Methods Tools - https://example.org/inputs/ + https://fmtools.fyi/inputs/ Recent content in Inputs on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CNF - https://example.org/inputs/cnf/ + https://fmtools.fyi/inputs/cnf/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/cnf/ + https://fmtools.fyi/inputs/cnf/ DIMACS - https://example.org/inputs/dimacs/ + https://fmtools.fyi/inputs/dimacs/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/dimacs/ + https://fmtools.fyi/inputs/dimacs/ Galileo - https://example.org/inputs/galileo/ + https://fmtools.fyi/inputs/galileo/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/galileo/ + https://fmtools.fyi/inputs/galileo/ GreatSPN - https://example.org/inputs/greatspn/ + https://fmtools.fyi/inputs/greatspn/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/greatspn/ + https://fmtools.fyi/inputs/greatspn/ JANI - https://example.org/inputs/jani/ + https://fmtools.fyi/inputs/jani/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/jani/ + https://fmtools.fyi/inputs/jani/ MRMC - https://example.org/inputs/mrmc/ + https://fmtools.fyi/inputs/mrmc/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/mrmc/ + https://fmtools.fyi/inputs/mrmc/ PNML - https://example.org/inputs/pnml/ + https://fmtools.fyi/inputs/pnml/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/pnml/ + https://fmtools.fyi/inputs/pnml/ PRISM - https://example.org/inputs/prism/ + https://fmtools.fyi/inputs/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/prism/ + https://fmtools.fyi/inputs/prism/ Sally - https://example.org/inputs/sally/ + https://fmtools.fyi/inputs/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/sally/ + https://fmtools.fyi/inputs/sally/ SMTLIB2 - https://example.org/inputs/smtlib2/ + https://fmtools.fyi/inputs/smtlib2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/smtlib2/ + https://fmtools.fyi/inputs/smtlib2/ Yices 2 - https://example.org/inputs/yices-2/ + https://fmtools.fyi/inputs/yices-2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/yices-2/ + https://fmtools.fyi/inputs/yices-2/ diff --git a/inputs/jani/index.html b/inputs/jani/index.html index f9907f8..17449c9 100644 --- a/inputs/jani/index.html +++ b/inputs/jani/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/jani/index.xml b/inputs/jani/index.xml index 2f6aacb..800f7f3 100644 --- a/inputs/jani/index.xml +++ b/inputs/jani/index.xml @@ -2,17 +2,17 @@ JANI on Formal Methods Tools - https://example.org/inputs/jani/ + https://fmtools.fyi/inputs/jani/ Recent content in JANI on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/inputs/mrmc/index.html b/inputs/mrmc/index.html index 650a2ef..d156df2 100644 --- a/inputs/mrmc/index.html +++ b/inputs/mrmc/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/mrmc/index.xml b/inputs/mrmc/index.xml index 15c2b64..acbd08a 100644 --- a/inputs/mrmc/index.xml +++ b/inputs/mrmc/index.xml @@ -2,24 +2,24 @@ MRMC on Formal Methods Tools - https://example.org/inputs/mrmc/ + https://fmtools.fyi/inputs/mrmc/ Recent content in MRMC on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/inputs/pnml/index.html b/inputs/pnml/index.html index 1033c33..ae508e1 100644 --- a/inputs/pnml/index.html +++ b/inputs/pnml/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/pnml/index.xml b/inputs/pnml/index.xml index 2dbc0ca..6ced9a9 100644 --- a/inputs/pnml/index.xml +++ b/inputs/pnml/index.xml @@ -2,17 +2,17 @@ PNML on Formal Methods Tools - https://example.org/inputs/pnml/ + https://fmtools.fyi/inputs/pnml/ Recent content in PNML on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/inputs/prism/index.html b/inputs/prism/index.html index a7c72cc..5bf591e 100644 --- a/inputs/prism/index.html +++ b/inputs/prism/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/prism/index.xml b/inputs/prism/index.xml index 0969280..0f26ef1 100644 --- a/inputs/prism/index.xml +++ b/inputs/prism/index.xml @@ -2,31 +2,31 @@ PRISM on Formal Methods Tools - https://example.org/inputs/prism/ + https://fmtools.fyi/inputs/prism/ Recent content in PRISM on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/inputs/sally/index.html b/inputs/sally/index.html index c7313d4..0db3012 100644 --- a/inputs/sally/index.html +++ b/inputs/sally/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/sally/index.xml b/inputs/sally/index.xml index 0258067..83001b4 100644 --- a/inputs/sally/index.xml +++ b/inputs/sally/index.xml @@ -2,17 +2,17 @@ Sally on Formal Methods Tools - https://example.org/inputs/sally/ + https://fmtools.fyi/inputs/sally/ Recent content in Sally on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> diff --git a/inputs/smtlib2/index.html b/inputs/smtlib2/index.html index 80e31bd..687f2f5 100644 --- a/inputs/smtlib2/index.html +++ b/inputs/smtlib2/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/smtlib2/index.xml b/inputs/smtlib2/index.xml index 2d7dfe6..5f8fe85 100644 --- a/inputs/smtlib2/index.xml +++ b/inputs/smtlib2/index.xml @@ -2,108 +2,108 @@ SMTLIB2 on Formal Methods Tools - https://example.org/inputs/smtlib2/ + https://fmtools.fyi/inputs/smtlib2/ Recent content in SMTLIB2 on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/inputs/yices-2/index.html b/inputs/yices-2/index.html index ebca481..e9827a2 100644 --- a/inputs/yices-2/index.html +++ b/inputs/yices-2/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/yices-2/index.xml b/inputs/yices-2/index.xml index 3c8c531..a58e7e2 100644 --- a/inputs/yices-2/index.xml +++ b/inputs/yices-2/index.xml @@ -2,17 +2,17 @@ Yices 2 on Formal Methods Tools - https://example.org/inputs/yices-2/ + https://fmtools.fyi/inputs/yices-2/ Recent content in Yices 2 on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> diff --git a/interfaces/.net/index.html b/interfaces/.net/index.html index 48c4b6f..9a663a9 100644 --- a/interfaces/.net/index.html +++ b/interfaces/.net/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/.net/index.xml b/interfaces/.net/index.xml index d6e0d17..7563afe 100644 --- a/interfaces/.net/index.xml +++ b/interfaces/.net/index.xml @@ -2,17 +2,17 @@ .NET on Formal Methods Tools - https://example.org/interfaces/.net/ + https://fmtools.fyi/interfaces/.net/ Recent content in .NET on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/c++/index.html b/interfaces/c++/index.html index c2f6b6c..dbd58fc 100644 --- a/interfaces/c++/index.html +++ b/interfaces/c++/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/c++/index.xml b/interfaces/c++/index.xml index 5154c6d..d77d7d4 100644 --- a/interfaces/c++/index.xml +++ b/interfaces/c++/index.xml @@ -2,38 +2,38 @@ C++ on Formal Methods Tools - https://example.org/interfaces/c++/ + https://fmtools.fyi/interfaces/c++/ Recent content in C++ on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/c/index.html b/interfaces/c/index.html index 8d8a627..974cc11 100644 --- a/interfaces/c/index.html +++ b/interfaces/c/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/c/index.xml b/interfaces/c/index.xml index a464320..b38276e 100644 --- a/interfaces/c/index.xml +++ b/interfaces/c/index.xml @@ -2,24 +2,24 @@ C on Formal Methods Tools - https://example.org/interfaces/c/ + https://fmtools.fyi/interfaces/c/ Recent content in C on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/cli/index.html b/interfaces/cli/index.html index dd43a2b..51a35a0 100644 --- a/interfaces/cli/index.html +++ b/interfaces/cli/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/cli/index.xml b/interfaces/cli/index.xml index 24234a8..a46dde0 100644 --- a/interfaces/cli/index.xml +++ b/interfaces/cli/index.xml @@ -2,185 +2,185 @@ CLI on Formal Methods Tools - https://example.org/interfaces/cli/ + https://fmtools.fyi/interfaces/cli/ Recent content in CLI on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> 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.</p> Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> Riss - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/index.html b/interfaces/index.html index 7f34cb7..f355821 100644 --- a/interfaces/index.html +++ b/interfaces/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/index.xml b/interfaces/index.xml index 94d4565..04224f0 100644 --- a/interfaces/index.xml +++ b/interfaces/index.xml @@ -2,66 +2,66 @@ Interfaces on Formal Methods Tools - https://example.org/interfaces/ + https://fmtools.fyi/interfaces/ Recent content in Interfaces on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + .NET - https://example.org/interfaces/.net/ + https://fmtools.fyi/interfaces/.net/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/.net/ + https://fmtools.fyi/interfaces/.net/ C - https://example.org/interfaces/c/ + https://fmtools.fyi/interfaces/c/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/c/ + https://fmtools.fyi/interfaces/c/ C++ - https://example.org/interfaces/c++/ + https://fmtools.fyi/interfaces/c++/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/c++/ + https://fmtools.fyi/interfaces/c++/ CLI - https://example.org/interfaces/cli/ + https://fmtools.fyi/interfaces/cli/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/cli/ + https://fmtools.fyi/interfaces/cli/ Java - https://example.org/interfaces/java/ + https://fmtools.fyi/interfaces/java/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/java/ + https://fmtools.fyi/interfaces/java/ Online - https://example.org/interfaces/online/ + https://fmtools.fyi/interfaces/online/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/online/ + https://fmtools.fyi/interfaces/online/ Python - https://example.org/interfaces/python/ + https://fmtools.fyi/interfaces/python/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/python/ + https://fmtools.fyi/interfaces/python/ Rust - https://example.org/interfaces/rust/ + https://fmtools.fyi/interfaces/rust/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/rust/ + https://fmtools.fyi/interfaces/rust/ diff --git a/interfaces/java/index.html b/interfaces/java/index.html index 17d1cfa..0c2f7ff 100644 --- a/interfaces/java/index.html +++ b/interfaces/java/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/java/index.xml b/interfaces/java/index.xml index 59721c9..3bc6a52 100644 --- a/interfaces/java/index.xml +++ b/interfaces/java/index.xml @@ -2,31 +2,31 @@ Java on Formal Methods Tools - https://example.org/interfaces/java/ + https://fmtools.fyi/interfaces/java/ Recent content in Java on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/online/index.html b/interfaces/online/index.html index 9fbaaf5..bee3405 100644 --- a/interfaces/online/index.html +++ b/interfaces/online/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/online/index.xml b/interfaces/online/index.xml index 88eaf28..7040e10 100644 --- a/interfaces/online/index.xml +++ b/interfaces/online/index.xml @@ -2,38 +2,38 @@ Online on Formal Methods Tools - https://example.org/interfaces/online/ + https://fmtools.fyi/interfaces/online/ Recent content in Online on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/python/index.html b/interfaces/python/index.html index a273ace..409eff9 100644 --- a/interfaces/python/index.html +++ b/interfaces/python/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/python/index.xml b/interfaces/python/index.xml index 2bf6240..e39434d 100644 --- a/interfaces/python/index.xml +++ b/interfaces/python/index.xml @@ -2,45 +2,45 @@ Python on Formal Methods Tools - https://example.org/interfaces/python/ + https://fmtools.fyi/interfaces/python/ Recent content in Python on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/rust/index.html b/interfaces/rust/index.html index 0b576c6..3f376a9 100644 --- a/interfaces/rust/index.html +++ b/interfaces/rust/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/rust/index.xml b/interfaces/rust/index.xml index 691b9f9..b2503dd 100644 --- a/interfaces/rust/index.xml +++ b/interfaces/rust/index.xml @@ -2,24 +2,24 @@ Rust on Formal Methods Tools - https://example.org/interfaces/rust/ + https://fmtools.fyi/interfaces/rust/ Recent content in Rust on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/license/index.html b/license/index.html index 980762b..9628871 100644 --- a/license/index.html +++ b/license/index.html @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/all-rights-reserved/index.html b/licenses/all-rights-reserved/index.html index 0243fb2..18543d9 100644 --- a/licenses/all-rights-reserved/index.html +++ b/licenses/all-rights-reserved/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/all-rights-reserved/index.xml b/licenses/all-rights-reserved/index.xml index ef314b9..2f55737 100644 --- a/licenses/all-rights-reserved/index.xml +++ b/licenses/all-rights-reserved/index.xml @@ -2,17 +2,17 @@ All Rights Reserved on Formal Methods Tools - https://example.org/licenses/all-rights-reserved/ + https://fmtools.fyi/licenses/all-rights-reserved/ Recent content in All Rights Reserved on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> diff --git a/licenses/apache-2.0/index.html b/licenses/apache-2.0/index.html index e58bac9..49cdae7 100644 --- a/licenses/apache-2.0/index.html +++ b/licenses/apache-2.0/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/apache-2.0/index.xml b/licenses/apache-2.0/index.xml index b9ed02c..17a5f4c 100644 --- a/licenses/apache-2.0/index.xml +++ b/licenses/apache-2.0/index.xml @@ -2,17 +2,17 @@ Apache-2.0 on Formal Methods Tools - https://example.org/licenses/apache-2.0/ + https://fmtools.fyi/licenses/apache-2.0/ Recent content in Apache-2.0 on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + dReal - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> 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.</p> diff --git a/licenses/bsd/index.html b/licenses/bsd/index.html index 474b3dd..921cce7 100644 --- a/licenses/bsd/index.html +++ b/licenses/bsd/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/bsd/index.xml b/licenses/bsd/index.xml index 6ef7472..9d2ecb7 100644 --- a/licenses/bsd/index.xml +++ b/licenses/bsd/index.xml @@ -2,31 +2,31 @@ BSD on Formal Methods Tools - https://example.org/licenses/bsd/ + https://fmtools.fyi/licenses/bsd/ Recent content in BSD on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> diff --git a/licenses/gplv2/index.html b/licenses/gplv2/index.html index 4d2b07a..b70d326 100644 --- a/licenses/gplv2/index.html +++ b/licenses/gplv2/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/gplv2/index.xml b/licenses/gplv2/index.xml index d4ac3c6..c926fff 100644 --- a/licenses/gplv2/index.xml +++ b/licenses/gplv2/index.xml @@ -2,31 +2,31 @@ GPLv2 on Formal Methods Tools - https://example.org/licenses/gplv2/ + https://fmtools.fyi/licenses/gplv2/ Recent content in GPLv2 on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> diff --git a/licenses/gplv3/index.html b/licenses/gplv3/index.html index ade2682..b4ee1d4 100644 --- a/licenses/gplv3/index.html +++ b/licenses/gplv3/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/gplv3/index.xml b/licenses/gplv3/index.xml index b8d2426..d73c207 100644 --- a/licenses/gplv3/index.xml +++ b/licenses/gplv3/index.xml @@ -2,52 +2,52 @@ GPLv3 on Formal Methods Tools - https://example.org/licenses/gplv3/ + https://fmtools.fyi/licenses/gplv3/ Recent content in GPLv3 on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> diff --git a/licenses/index.html b/licenses/index.html index ed5f4ea..b211a35 100644 --- a/licenses/index.html +++ b/licenses/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/index.xml b/licenses/index.xml index b5a643e..4a08a10 100644 --- a/licenses/index.xml +++ b/licenses/index.xml @@ -2,59 +2,59 @@ Licenses on Formal Methods Tools - https://example.org/licenses/ + https://fmtools.fyi/licenses/ Recent content in Licenses on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + All Rights Reserved - https://example.org/licenses/all-rights-reserved/ + https://fmtools.fyi/licenses/all-rights-reserved/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/all-rights-reserved/ + https://fmtools.fyi/licenses/all-rights-reserved/ Apache-2.0 - https://example.org/licenses/apache-2.0/ + https://fmtools.fyi/licenses/apache-2.0/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/apache-2.0/ + https://fmtools.fyi/licenses/apache-2.0/ BSD - https://example.org/licenses/bsd/ + https://fmtools.fyi/licenses/bsd/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/bsd/ + https://fmtools.fyi/licenses/bsd/ GPLv2 - https://example.org/licenses/gplv2/ + https://fmtools.fyi/licenses/gplv2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/gplv2/ + https://fmtools.fyi/licenses/gplv2/ GPLv3 - https://example.org/licenses/gplv3/ + https://fmtools.fyi/licenses/gplv3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/gplv3/ + https://fmtools.fyi/licenses/gplv3/ LGPLv2 - https://example.org/licenses/lgplv2/ + https://fmtools.fyi/licenses/lgplv2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/lgplv2/ + https://fmtools.fyi/licenses/lgplv2/ MIT - https://example.org/licenses/mit/ + https://fmtools.fyi/licenses/mit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/mit/ + https://fmtools.fyi/licenses/mit/ diff --git a/licenses/lgplv2/index.html b/licenses/lgplv2/index.html index 103c84f..c2a0084 100644 --- a/licenses/lgplv2/index.html +++ b/licenses/lgplv2/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/lgplv2/index.xml b/licenses/lgplv2/index.xml index 8991086..f44348c 100644 --- a/licenses/lgplv2/index.xml +++ b/licenses/lgplv2/index.xml @@ -2,17 +2,17 @@ LGPLv2 on Formal Methods Tools - https://example.org/licenses/lgplv2/ + https://fmtools.fyi/licenses/lgplv2/ Recent content in LGPLv2 on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Riss - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> diff --git a/licenses/mit/index.html b/licenses/mit/index.html index 287def3..cb311f4 100644 --- a/licenses/mit/index.html +++ b/licenses/mit/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/mit/index.xml b/licenses/mit/index.xml index 27f50c0..77fbaf5 100644 --- a/licenses/mit/index.xml +++ b/licenses/mit/index.xml @@ -2,94 +2,94 @@ MIT on Formal Methods Tools - https://example.org/licenses/mit/ + https://fmtools.fyi/licenses/mit/ Recent content in MIT on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/maintenance/actively-maintained/index.html b/maintenance/actively-maintained/index.html index 2532944..b8f1cf6 100644 --- a/maintenance/actively-maintained/index.html +++ b/maintenance/actively-maintained/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/maintenance/actively-maintained/index.xml b/maintenance/actively-maintained/index.xml index a67a441..7c66ded 100644 --- a/maintenance/actively-maintained/index.xml +++ b/maintenance/actively-maintained/index.xml @@ -2,143 +2,143 @@ Actively Maintained on Formal Methods Tools - https://example.org/maintenance/actively-maintained/ + https://fmtools.fyi/maintenance/actively-maintained/ Recent content in Actively Maintained on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/maintenance/index.html b/maintenance/index.html index ed158f8..1134397 100644 --- a/maintenance/index.html +++ b/maintenance/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/maintenance/index.xml b/maintenance/index.xml index b99557d..9478205 100644 --- a/maintenance/index.xml +++ b/maintenance/index.xml @@ -2,24 +2,24 @@ Maintenance on Formal Methods Tools - https://example.org/maintenance/ + https://fmtools.fyi/maintenance/ Recent content in Maintenance on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Actively Maintained - https://example.org/maintenance/actively-maintained/ + https://fmtools.fyi/maintenance/actively-maintained/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/maintenance/actively-maintained/ + https://fmtools.fyi/maintenance/actively-maintained/ Not Maintained - https://example.org/maintenance/not-maintained/ + https://fmtools.fyi/maintenance/not-maintained/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/maintenance/not-maintained/ + https://fmtools.fyi/maintenance/not-maintained/ diff --git a/maintenance/not-maintained/index.html b/maintenance/not-maintained/index.html index eea71fe..0d004ac 100644 --- a/maintenance/not-maintained/index.html +++ b/maintenance/not-maintained/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/maintenance/not-maintained/index.xml b/maintenance/not-maintained/index.xml index 5504f82..60a5f2e 100644 --- a/maintenance/not-maintained/index.xml +++ b/maintenance/not-maintained/index.xml @@ -2,52 +2,52 @@ Not Maintained on Formal Methods Tools - https://example.org/maintenance/not-maintained/ + https://fmtools.fyi/maintenance/not-maintained/ Recent content in Not Maintained on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> dReal - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> 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.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> Riss - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> diff --git a/privacy/index.html b/privacy/index.html index 86a5538..a2ec1a9 100644 --- a/privacy/index.html +++ b/privacy/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/sitemap.xml b/sitemap.xml index 5676bc8..e7d8bc3 100644 --- a/sitemap.xml +++ b/sitemap.xml @@ -2,316 +2,316 @@ - https://example.org/interfaces/.net/ + https://fmtools.fyi/interfaces/.net/ 2025-06-07T00:00:00+00:00 - https://example.org/maintenance/actively-maintained/ + https://fmtools.fyi/maintenance/actively-maintained/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/albert-ludwigs-universit%C3%A4t/ + https://fmtools.fyi/developers/albert-ludwigs-universit%C3%A4t/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/all-rights-reserved/ + https://fmtools.fyi/licenses/all-rights-reserved/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/ + https://fmtools.fyi/tools/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/apache-2.0/ + https://fmtools.fyi/licenses/apache-2.0/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/ + https://fmtools.fyi/applications/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/bsd/ + https://fmtools.fyi/licenses/bsd/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/c/ + https://fmtools.fyi/interfaces/c/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/c++/ + https://fmtools.fyi/interfaces/c++/ 2025-06-07T00:00:00+00:00 - https://example.org/techniques/cdcl/ + https://fmtools.fyi/techniques/cdcl/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/cea/ + https://fmtools.fyi/developers/cea/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/cli/ + https://fmtools.fyi/interfaces/cli/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/cnf/ + https://fmtools.fyi/inputs/cnf/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/constraint-solver/ + https://fmtools.fyi/applications/constraint-solver/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/ + https://fmtools.fyi/developers/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/dimacs/ + https://fmtools.fyi/inputs/dimacs/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/disi-university-of-trento/ + https://fmtools.fyi/developers/disi-university-of-trento/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/eindhoven-university-of-technology/ + https://fmtools.fyi/developers/eindhoven-university-of-technology/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/fondazione-bruno-kessler/ + https://fmtools.fyi/developers/fondazione-bruno-kessler/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/galileo/ + https://fmtools.fyi/inputs/galileo/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/gilles-audemard/ + https://fmtools.fyi/developers/gilles-audemard/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/gplv2/ + https://fmtools.fyi/licenses/gplv2/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/gplv3/ + https://fmtools.fyi/licenses/gplv3/ 2025-06-07T00:00:00+00:00 - https://example.org/techniques/gpu/ + https://fmtools.fyi/techniques/gpu/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/greatspn/ + https://fmtools.fyi/inputs/greatspn/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/ + https://fmtools.fyi/inputs/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/inria-rh%C3%B4ne-alpes/ + https://fmtools.fyi/developers/inria-rh%C3%B4ne-alpes/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/ + https://fmtools.fyi/interfaces/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/jani/ + https://fmtools.fyi/inputs/jani/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/java/ + https://fmtools.fyi/interfaces/java/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/johannes-kepler-universit%C3%A4t-linz/ + https://fmtools.fyi/developers/johannes-kepler-universit%C3%A4t-linz/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/laurent-simon/ + https://fmtools.fyi/developers/laurent-simon/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/lgplv2/ + https://fmtools.fyi/licenses/lgplv2/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/ + https://fmtools.fyi/licenses/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/loria/ + https://fmtools.fyi/developers/loria/ 2025-06-07T00:00:00+00:00 - https://example.org/maintenance/ + https://fmtools.fyi/maintenance/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/masaryk-university/ + https://fmtools.fyi/developers/masaryk-university/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/microsoft-research/ + https://fmtools.fyi/developers/microsoft-research/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/mit/ + https://fmtools.fyi/licenses/mit/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/model-checker/ + https://fmtools.fyi/applications/model-checker/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/mc/ + https://fmtools.fyi/tools/mc/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/mrmc/ + https://fmtools.fyi/inputs/mrmc/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/niklas-e%C3%A9n/ + https://fmtools.fyi/developers/niklas-e%C3%A9n/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/niklas-s%C3%B6rensson/ + https://fmtools.fyi/developers/niklas-s%C3%B6rensson/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/norbert-manthey/ + https://fmtools.fyi/developers/norbert-manthey/ 2025-06-07T00:00:00+00:00 - https://example.org/maintenance/not-maintained/ + https://fmtools.fyi/maintenance/not-maintained/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/online/ + https://fmtools.fyi/interfaces/online/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/oxford-university/ + https://fmtools.fyi/developers/oxford-university/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/pnml/ + https://fmtools.fyi/inputs/pnml/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/prism/ + https://fmtools.fyi/inputs/prism/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/probabilistic-model-checker/ + https://fmtools.fyi/applications/probabilistic-model-checker/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/prob/ + https://fmtools.fyi/tools/prob/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/python/ + https://fmtools.fyi/interfaces/python/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/rust/ + https://fmtools.fyi/interfaces/rust/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/rwth-aachen/ + https://fmtools.fyi/developers/rwth-aachen/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/sally/ + https://fmtools.fyi/inputs/sally/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/ + https://fmtools.fyi/tools/sat-smt/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/sat-solver/ + https://fmtools.fyi/applications/sat-solver/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/smt-solver/ + https://fmtools.fyi/applications/smt-solver/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/smtlib2/ + https://fmtools.fyi/inputs/smtlib2/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/sri-international/ + https://fmtools.fyi/developers/sri-international/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/stanford-university/ + https://fmtools.fyi/developers/stanford-university/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ 2025-06-07T00:00:00+00:00 - https://example.org/techniques/ + https://fmtools.fyi/techniques/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/termination/ + https://fmtools.fyi/tools/termination/ 2025-06-07T00:00:00+00:00 - https://example.org/ + https://fmtools.fyi/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/theorem-prover/ + https://fmtools.fyi/applications/theorem-prover/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/uliege/ + https://fmtools.fyi/developers/uliege/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-freiburg/ + https://fmtools.fyi/developers/university-of-freiburg/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-illinois/ + https://fmtools.fyi/developers/university-of-illinois/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-iowa/ + https://fmtools.fyi/developers/university-of-iowa/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-lugano/ + https://fmtools.fyi/developers/university-of-lugano/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-virginia/ + https://fmtools.fyi/developers/university-of-virginia/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/utah-state-university/ + https://fmtools.fyi/developers/utah-state-university/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/yices-2/ + https://fmtools.fyi/inputs/yices-2/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ 2025-06-07T00:00:00+00:00 - https://example.org/about/ + https://fmtools.fyi/about/ - https://example.org/taxonomies/ + https://fmtools.fyi/taxonomies/ - https://example.org/contribute/ + https://fmtools.fyi/contribute/ - https://example.org/domains/ + https://fmtools.fyi/domains/ - https://example.org/license/ + https://fmtools.fyi/license/ - https://example.org/privacy/ + https://fmtools.fyi/privacy/ diff --git a/taxonomies/index.html b/taxonomies/index.html index ed3a4c1..a747836 100644 --- a/taxonomies/index.html +++ b/taxonomies/index.html @@ -15,16 +15,16 @@ - + - + - - - - + + + + - + diff --git a/taxonomies/index.xml b/taxonomies/index.xml index 19d5fe8..77ea3ad 100644 --- a/taxonomies/index.xml +++ b/taxonomies/index.xml @@ -2,10 +2,10 @@ All Taxonomy Data on Formal Methods Tools - https://example.org/taxonomies/ + https://fmtools.fyi/taxonomies/ Recent content in All Taxonomy Data on Formal Methods Tools Hugo en-us - + diff --git a/techniques/cdcl/index.html b/techniques/cdcl/index.html index 05c7ada..26de6e8 100644 --- a/techniques/cdcl/index.html +++ b/techniques/cdcl/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/techniques/cdcl/index.xml b/techniques/cdcl/index.xml index ad58d3c..ff67f62 100644 --- a/techniques/cdcl/index.xml +++ b/techniques/cdcl/index.xml @@ -2,17 +2,17 @@ CDCL on Formal Methods Tools - https://example.org/techniques/cdcl/ + https://fmtools.fyi/techniques/cdcl/ Recent content in CDCL on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/techniques/gpu/index.html b/techniques/gpu/index.html index 22cba3a..bb9b3ef 100644 --- a/techniques/gpu/index.html +++ b/techniques/gpu/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/techniques/gpu/index.xml b/techniques/gpu/index.xml index d71124a..ffb98ff 100644 --- a/techniques/gpu/index.xml +++ b/techniques/gpu/index.xml @@ -2,17 +2,17 @@ GPU on Formal Methods Tools - https://example.org/techniques/gpu/ + https://fmtools.fyi/techniques/gpu/ Recent content in GPU on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/techniques/index.html b/techniques/index.html index 5f138eb..9042265 100644 --- a/techniques/index.html +++ b/techniques/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/techniques/index.xml b/techniques/index.xml index 92394f1..c7fa838 100644 --- a/techniques/index.xml +++ b/techniques/index.xml @@ -2,24 +2,24 @@ Techniques on Formal Methods Tools - https://example.org/techniques/ + https://fmtools.fyi/techniques/ Recent content in Techniques on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + CDCL - https://example.org/techniques/cdcl/ + https://fmtools.fyi/techniques/cdcl/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/techniques/cdcl/ + https://fmtools.fyi/techniques/cdcl/ GPU - https://example.org/techniques/gpu/ + https://fmtools.fyi/techniques/gpu/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/techniques/gpu/ + https://fmtools.fyi/techniques/gpu/ diff --git a/tools/index.html b/tools/index.html index 7c993bd..02dc7d2 100644 --- a/tools/index.html +++ b/tools/index.html @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/index.xml b/tools/index.xml index 8c61c25..51463cf 100644 --- a/tools/index.xml +++ b/tools/index.xml @@ -2,11 +2,11 @@ All Tools on Formal Methods Tools - https://example.org/tools/ + https://fmtools.fyi/tools/ Recent content in All Tools on Formal Methods Tools Hugo en-us - + diff --git a/tools/mc/index.html b/tools/mc/index.html index ab9cb5d..0cce452 100644 --- a/tools/mc/index.html +++ b/tools/mc/index.html @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/mc/index.xml b/tools/mc/index.xml index 9d8b32f..62b0103 100644 --- a/tools/mc/index.xml +++ b/tools/mc/index.xml @@ -2,17 +2,17 @@ Model Checking Tools on Formal Methods Tools - https://example.org/tools/mc/ + https://fmtools.fyi/tools/mc/ Recent content in Model Checking Tools on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Sally - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/mc/sally/ + https://fmtools.fyi/tools/mc/sally/ <p>Sally is a model checker for infinite state systems described as transition systems.</p> diff --git a/tools/mc/sally/index.html b/tools/mc/sally/index.html index f4e4344..0272a19 100644 --- a/tools/mc/sally/index.html +++ b/tools/mc/sally/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/prob/index.html b/tools/prob/index.html index b52a47f..b453a5c 100644 --- a/tools/prob/index.html +++ b/tools/prob/index.html @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/prob/index.xml b/tools/prob/index.xml index 479b002..80accba 100644 --- a/tools/prob/index.xml +++ b/tools/prob/index.xml @@ -2,31 +2,31 @@ Probabilistic Tools on Formal Methods Tools - https://example.org/tools/prob/ + https://fmtools.fyi/tools/prob/ Recent content in Probabilistic Tools on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + PRISM - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/prism/ + https://fmtools.fyi/tools/prob/prism/ <p>PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.</p> STAMINA - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/stamina/ + https://fmtools.fyi/tools/prob/stamina/ <p>A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either <a href="../storm" >Storm</a> or <a href="../prism" >PRISM</a>.</p> Storm - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/prob/storm/ + https://fmtools.fyi/tools/prob/storm/ <p>Storm is a tool for the analysis of systems involving random or probabilistic phenomena.</p> diff --git a/tools/prob/prism/index.html b/tools/prob/prism/index.html index ccb14f7..c9a1c45 100644 --- a/tools/prob/prism/index.html +++ b/tools/prob/prism/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/prob/stamina/index.html b/tools/prob/stamina/index.html index 46f8455..5dea995 100644 --- a/tools/prob/stamina/index.html +++ b/tools/prob/stamina/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/prob/storm/index.html b/tools/prob/storm/index.html index 75fa459..480d44c 100644 --- a/tools/prob/storm/index.html +++ b/tools/prob/storm/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/bitwuzla/index.html b/tools/sat-smt/bitwuzla/index.html index 7cc23be..ac9cf0b 100644 --- a/tools/sat-smt/bitwuzla/index.html +++ b/tools/sat-smt/bitwuzla/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/boolector/index.html b/tools/sat-smt/boolector/index.html index f395ced..de01bf5 100644 --- a/tools/sat-smt/boolector/index.html +++ b/tools/sat-smt/boolector/index.html @@ -24,16 +24,16 @@ ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size"> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/colibri/index.html b/tools/sat-smt/colibri/index.html index e8be45a..621cfc0 100644 --- a/tools/sat-smt/colibri/index.html +++ b/tools/sat-smt/colibri/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/cryptominisat/index.html b/tools/sat-smt/cryptominisat/index.html index 76566a3..57a2a8b 100644 --- a/tools/sat-smt/cryptominisat/index.html +++ b/tools/sat-smt/cryptominisat/index.html @@ -19,16 +19,16 @@ This tool is available through the following interfaces: C++ Namespace: Documentation on homepage Python"> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/cvc4/index.html b/tools/sat-smt/cvc4/index.html index 415cc17..a2bd266 100644 --- a/tools/sat-smt/cvc4/index.html +++ b/tools/sat-smt/cvc4/index.html @@ -24,16 +24,16 @@ ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5"> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/cvc5/index.html b/tools/sat-smt/cvc5/index.html index f21fb90..c44a399 100644 --- a/tools/sat-smt/cvc5/index.html +++ b/tools/sat-smt/cvc5/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/dreal/index.html b/tools/sat-smt/dreal/index.html index 826f41a..00293fe 100644 --- a/tools/sat-smt/dreal/index.html +++ b/tools/sat-smt/dreal/index.html @@ -24,16 +24,16 @@ ] dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as"> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/glucose/index.html b/tools/sat-smt/glucose/index.html index 5dda277..2dd2614 100644 --- a/tools/sat-smt/glucose/index.html +++ b/tools/sat-smt/glucose/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/index.html b/tools/sat-smt/index.html index 6a19a3b..679d639 100644 --- a/tools/sat-smt/index.html +++ b/tools/sat-smt/index.html @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/index.xml b/tools/sat-smt/index.xml index 386c34f..e5f2769 100644 --- a/tools/sat-smt/index.xml +++ b/tools/sat-smt/index.xml @@ -2,157 +2,157 @@ SAT & SMT Tools on Formal Methods Tools - https://example.org/tools/sat-smt/ + https://fmtools.fyi/tools/sat-smt/ Recent content in SAT & SMT Tools on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Bitwuzla - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + https://fmtools.fyi/tools/sat-smt/bitwuzla/ <p>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.</p> Boolector - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + https://fmtools.fyi/tools/sat-smt/boolector/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2024</span> <span style="display:none">]</span> </div> Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. Succeeded by <a href="../bitwuzla" >Bitwuzla</a></p> Colibri - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + https://fmtools.fyi/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + https://fmtools.fyi/tools/sat-smt/cryptominisat/ <p>CryptoMiniSat is a SAT solver.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ Namespace:</strong> Documentation on <a href="https://www.msoos.org/cryptominisat5/" target="_blank" >homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/" target="_blank" >PyPI package</a></li> </ul> cvc4 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + https://fmtools.fyi/tools/sat-smt/cvc4/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2021</span> <span style="display:none">]</span> </div> cvc4 is an automatic theorem prover for SMT problems. It is succeeded by <a href="../cvc5" >cvc5</a></p> cvc5 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + https://fmtools.fyi/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + https://fmtools.fyi/tools/sat-smt/dreal/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> 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.</p> Glucose - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + https://fmtools.fyi/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + https://fmtools.fyi/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + https://fmtools.fyi/tools/sat-smt/mathsat/ <p><div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(226, 181, 59);"></span> <span style="display:none">[</span> <span style="color: rgb(226, 181, 59); font-size: 1rem;">Closed-Source Tool</span> <span style="display:none">]&nbsp;</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + https://fmtools.fyi/tools/sat-smt/minisat/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2013</span> <span style="display:none">]</span> </div> MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> OpenSMT - https://example.org/tools/sat-smt/opensmt/ + https://fmtools.fyi/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/opensmt/ - <p>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 <a href="https://example.org/tools/minisat" >MiniSAT</a>.</p> + https://fmtools.fyi/tools/sat-smt/opensmt/ + <p>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 <a href="https://fmtools.fyi/tools/minisat" >MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + https://fmtools.fyi/tools/sat-smt/parafrost/ <p>ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> Q3B - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + https://fmtools.fyi/tools/sat-smt/q3b/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2023</span> <span style="display:none">]</span> </div> Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.</p> Riss - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + https://fmtools.fyi/tools/sat-smt/riss/ <p> <div style="display: flex; align-items: center; gap: 8px;"> <span style="display: inline-block; width: 12px; height: 12px; border-radius: 50%; background: rgb(240, 85, 85);"></span> <span style="display:none">[</span> <span style="color: rgb(240, 85, 85); font-size: 1rem;">Not Maintained Since 2017</span> <span style="display:none">]</span> </div> Riss is a SAT solving tool collection.</p> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + https://fmtools.fyi/tools/sat-smt/smt-rat/ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25" target="_blank" >C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + https://fmtools.fyi/tools/sat-smt/smtinterpol/ <p>SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>Java API:</strong> <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" target="_blank" >Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + https://fmtools.fyi/tools/sat-smt/stp/ <p>STP is a constraint solver for quantifier-free bitvectors.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage" target="_blank" >stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage" target="_blank" >stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + https://fmtools.fyi/tools/sat-smt/verit/ <p>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.</p> Yices 2 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + https://fmtools.fyi/tools/sat-smt/yices/ <p>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.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html" target="_blank" >Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/" target="_blank" >yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2" target="_blank" >yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + https://fmtools.fyi/tools/sat-smt/z3/ <p>Z3 is a general-purpose theorem prover widely used for SAT &amp; SMT solving.</p> <h2 id="apis-and-bindings">APIs and Bindings</h2> <p>This tool is available through the following interfaces:</p> <ul> <li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html" target="_blank" >Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html" target="_blank" >Z3 C++ Namespace Reference</a></li> <li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html" target="_blank" >Z3 .NET Namespace Reference</a></li> <li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html" target="_blank" >Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/" target="_blank" >z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html" target="_blank" >Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3" target="_blank" >z3 crate on crates.io</a></li> </ul> diff --git a/tools/sat-smt/lingeling/index.html b/tools/sat-smt/lingeling/index.html index 5d54af6..d91125c 100644 --- a/tools/sat-smt/lingeling/index.html +++ b/tools/sat-smt/lingeling/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/mathsat/index.html b/tools/sat-smt/mathsat/index.html index dccaa70..b600244 100644 --- a/tools/sat-smt/mathsat/index.html +++ b/tools/sat-smt/mathsat/index.html @@ -20,16 +20,16 @@ ]  MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get"> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/minisat/index.html b/tools/sat-smt/minisat/index.html index 6bb7133..be22ca6 100644 --- a/tools/sat-smt/minisat/index.html +++ b/tools/sat-smt/minisat/index.html @@ -24,16 +24,16 @@ ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers"> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/opensmt/index.html b/tools/sat-smt/opensmt/index.html index af8c1ae..81406c1 100644 --- a/tools/sat-smt/opensmt/index.html +++ b/tools/sat-smt/opensmt/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/parafrost/index.html b/tools/sat-smt/parafrost/index.html index 2a38c86..262dd6f 100644 --- a/tools/sat-smt/parafrost/index.html +++ b/tools/sat-smt/parafrost/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/q3b/index.html b/tools/sat-smt/q3b/index.html index 8939783..c31a990 100644 --- a/tools/sat-smt/q3b/index.html +++ b/tools/sat-smt/q3b/index.html @@ -24,16 +24,16 @@ ] Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs."> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/riss/index.html b/tools/sat-smt/riss/index.html index 4b33fbc..43c9451 100644 --- a/tools/sat-smt/riss/index.html +++ b/tools/sat-smt/riss/index.html @@ -24,16 +24,16 @@ ] Riss is a SAT solving tool collection."> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/smt-rat/index.html b/tools/sat-smt/smt-rat/index.html index 84e1ed8..16c54a1 100644 --- a/tools/sat-smt/smt-rat/index.html +++ b/tools/sat-smt/smt-rat/index.html @@ -19,16 +19,16 @@ This tool is available through the following interfaces: C++ API: C++ API Reference "> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/smtinterpol/index.html b/tools/sat-smt/smtinterpol/index.html index fb0dd8a..3bc1053 100644 --- a/tools/sat-smt/smtinterpol/index.html +++ b/tools/sat-smt/smtinterpol/index.html @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/stp/index.html b/tools/sat-smt/stp/index.html index 21d4658..3d63d69 100644 --- a/tools/sat-smt/stp/index.html +++ b/tools/sat-smt/stp/index.html @@ -18,16 +18,16 @@ APIs and Bindings This tool is available through the following interfaces: C API: stp C API"> - + - + - - - - + + + + - + diff --git a/tools/sat-smt/verit/index.html b/tools/sat-smt/verit/index.html index 8a19359..c4eab38 100644 --- a/tools/sat-smt/verit/index.html +++ b/tools/sat-smt/verit/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/yices/index.html b/tools/sat-smt/yices/index.html index 18503c5..dd4b457 100644 --- a/tools/sat-smt/yices/index.html +++ b/tools/sat-smt/yices/index.html @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/z3/index.html b/tools/sat-smt/z3/index.html index 7e215d8..9680ae6 100644 --- a/tools/sat-smt/z3/index.html +++ b/tools/sat-smt/z3/index.html @@ -18,16 +18,16 @@ APIs and Bindings This tool is available through the following interfaces: C API:"> - + - + - - - - + + + + - + diff --git a/tools/termination/index.html b/tools/termination/index.html index 7c5343e..fb80e4f 100644 --- a/tools/termination/index.html +++ b/tools/termination/index.html @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/termination/index.xml b/tools/termination/index.xml index f1fc399..a04e186 100644 --- a/tools/termination/index.xml +++ b/tools/termination/index.xml @@ -2,11 +2,11 @@ Termination Tools on Formal Methods Tools - https://example.org/tools/termination/ + https://fmtools.fyi/tools/termination/ Recent content in Termination Tools on Formal Methods Tools Hugo en-us - +