From ad8d224db4b52377934ca4cdaf9302083c6b814a Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Thu, 12 Jun 2025 15:31:42 -0600 Subject: [PATCH] Add git links --- 404.html | 16 +- about/index.html | 16 +- applications/constraint-solver/index.html | 16 +- applications/constraint-solver/index.xml | 8 +- applications/index.html | 16 +- applications/index.xml | 20 +- applications/sat-solver/index.html | 16 +- applications/sat-solver/index.xml | 48 ++-- applications/smt-solver/index.html | 16 +- applications/smt-solver/index.xml | 66 ++--- applications/theorem-prover/index.html | 16 +- applications/theorem-prover/index.xml | 28 +- contribute/index.html | 26 +- .../albert-ludwigs-universität/index.html | 16 +- .../albert-ludwigs-universität/index.xml | 8 +- developers/cea/index.html | 16 +- developers/cea/index.xml | 8 +- .../disi-university-of-trento/index.html | 16 +- .../disi-university-of-trento/index.xml | 8 +- .../index.html | 16 +- .../index.xml | 8 +- .../fondazione-bruno-kessler/index.html | 16 +- developers/fondazione-bruno-kessler/index.xml | 8 +- developers/gilles-audemard/index.html | 16 +- developers/gilles-audemard/index.xml | 8 +- developers/index.html | 16 +- developers/index.xml | 100 ++++---- developers/inria-rhône-alpes/index.html | 16 +- developers/inria-rhône-alpes/index.xml | 8 +- .../index.html | 16 +- .../index.xml | 12 +- developers/laurent-simon/index.html | 16 +- developers/laurent-simon/index.xml | 8 +- developers/loria/index.html | 16 +- developers/loria/index.xml | 8 +- developers/masaryk-university/index.html | 16 +- developers/masaryk-university/index.xml | 8 +- developers/microsoft-research/index.html | 16 +- developers/microsoft-research/index.xml | 8 +- developers/niklas-eén/index.html | 16 +- developers/niklas-eén/index.xml | 8 +- developers/niklas-sörensson/index.html | 16 +- developers/niklas-sörensson/index.xml | 8 +- developers/norbert-manthey/index.html | 16 +- developers/norbert-manthey/index.xml | 8 +- developers/rwth-aachen/index.html | 16 +- developers/rwth-aachen/index.xml | 8 +- developers/sri-international/index.html | 16 +- developers/sri-international/index.xml | 8 +- developers/stanford-university/index.html | 16 +- developers/stanford-university/index.xml | 24 +- developers/uliege/index.html | 16 +- developers/uliege/index.xml | 8 +- developers/university-of-freiburg/index.html | 16 +- developers/university-of-freiburg/index.xml | 8 +- developers/university-of-illinois/index.html | 16 +- developers/university-of-illinois/index.xml | 8 +- developers/university-of-iowa/index.html | 16 +- developers/university-of-iowa/index.xml | 12 +- developers/university-of-lugano/index.html | 16 +- developers/university-of-lugano/index.xml | 10 +- developers/university-of-virginia/index.html | 16 +- developers/university-of-virginia/index.xml | 8 +- domains/index.html | 16 +- domains/index.xml | 4 +- index.html | 241 +++++++++--------- index.xml | 108 ++++---- inputs/cnf/index.html | 16 +- inputs/cnf/index.xml | 12 +- inputs/dimacs/index.html | 16 +- inputs/dimacs/index.xml | 12 +- inputs/index.html | 16 +- inputs/index.xml | 20 +- inputs/smtlib2/index.html | 16 +- inputs/smtlib2/index.xml | 62 ++--- inputs/yices-2/index.html | 16 +- inputs/yices-2/index.xml | 8 +- interfaces/.net/index.html | 16 +- interfaces/.net/index.xml | 8 +- interfaces/c++/index.html | 16 +- interfaces/c++/index.xml | 16 +- interfaces/c/index.html | 16 +- interfaces/c/index.xml | 12 +- interfaces/cli/index.html | 16 +- interfaces/cli/index.xml | 90 +++---- interfaces/index.html | 16 +- interfaces/index.xml | 36 +-- interfaces/java/index.html | 16 +- interfaces/java/index.xml | 12 +- interfaces/online/index.html | 16 +- interfaces/online/index.xml | 16 +- interfaces/python/index.html | 16 +- interfaces/python/index.xml | 20 +- interfaces/rust/index.html | 16 +- interfaces/rust/index.xml | 12 +- license/index.html | 16 +- licenses/all-rights-reserved/index.html | 16 +- licenses/all-rights-reserved/index.xml | 8 +- licenses/apache-2.0/index.html | 16 +- licenses/apache-2.0/index.xml | 8 +- licenses/bsd/index.html | 16 +- licenses/bsd/index.xml | 16 +- licenses/gplv2/index.html | 16 +- licenses/gplv2/index.xml | 8 +- licenses/gplv3/index.html | 16 +- licenses/gplv3/index.xml | 22 +- licenses/index.html | 16 +- licenses/index.xml | 32 +-- licenses/lgplv2/index.html | 16 +- licenses/lgplv2/index.xml | 8 +- licenses/mit/index.html | 16 +- licenses/mit/index.xml | 48 ++-- maintenance/actively-maintained/index.html | 16 +- maintenance/actively-maintained/index.xml | 66 ++--- maintenance/index.html | 16 +- maintenance/index.xml | 12 +- maintenance/not-maintained/index.html | 16 +- maintenance/not-maintained/index.xml | 28 +- privacy/index.html | 16 +- sitemap.xml | 180 ++++++------- taxonomies/index.html | 16 +- taxonomies/index.xml | 4 +- techniques/cdcl/index.html | 16 +- techniques/cdcl/index.xml | 8 +- techniques/gpu/index.html | 16 +- techniques/gpu/index.xml | 8 +- techniques/index.html | 16 +- techniques/index.xml | 12 +- tools/index.html | 100 ++++---- tools/index.xml | 4 +- tools/pmc/index.html | 16 +- tools/pmc/index.xml | 4 +- tools/sat-smt/bitwuzla/index.html | 20 +- tools/sat-smt/boolector/index.html | 16 +- tools/sat-smt/colibri/index.html | 16 +- tools/sat-smt/cryptominisat/index.html | 16 +- tools/sat-smt/cvc4/index.html | 16 +- tools/sat-smt/cvc5/index.html | 16 +- tools/sat-smt/dreal/index.html | 16 +- tools/sat-smt/glucose/index.html | 16 +- tools/sat-smt/index.html | 16 +- tools/sat-smt/index.xml | 90 +++---- tools/sat-smt/lingeling/index.html | 16 +- tools/sat-smt/mathsat/index.html | 16 +- tools/sat-smt/minisat/index.html | 16 +- tools/sat-smt/opensmt/index.html | 16 +- tools/sat-smt/parafrost/index.html | 16 +- tools/sat-smt/q3b/index.html | 16 +- tools/sat-smt/riss/index.html | 16 +- tools/sat-smt/smt-rat/index.html | 16 +- tools/sat-smt/smtinterpol/index.html | 16 +- tools/sat-smt/stp/index.html | 16 +- tools/sat-smt/verit/index.html | 16 +- tools/sat-smt/yices/index.html | 16 +- tools/sat-smt/z3/index.html | 16 +- tools/termination/index.html | 16 +- tools/termination/index.xml | 4 +- 157 files changed, 1648 insertions(+), 1637 deletions(-) diff --git a/404.html b/404.html index 79c23dc..539cb1d 100644 --- a/404.html +++ b/404.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/about/index.html b/about/index.html index 569b551..43d0164 100644 --- a/about/index.html +++ b/about/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/constraint-solver/index.html b/applications/constraint-solver/index.html index fd26f5a..5f4733b 100644 --- a/applications/constraint-solver/index.html +++ b/applications/constraint-solver/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/constraint-solver/index.xml b/applications/constraint-solver/index.xml index fd169a4..7b0a509 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> diff --git a/applications/index.html b/applications/index.html index f14fa96..46e44a6 100644 --- a/applications/index.html +++ b/applications/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/index.xml b/applications/index.xml index 4132ce0..56f8230 100644 --- a/applications/index.xml +++ b/applications/index.xml @@ -2,38 +2,38 @@ Applications on Formal Methods Tools - https://example.org/applications/ + http://localhost:1313/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/ + http://localhost:1313/applications/constraint-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/constraint-solver/ + http://localhost:1313/applications/constraint-solver/ SAT Solver - https://example.org/applications/sat-solver/ + http://localhost:1313/applications/sat-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/sat-solver/ + http://localhost:1313/applications/sat-solver/ SMT Solver - https://example.org/applications/smt-solver/ + http://localhost:1313/applications/smt-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/smt-solver/ + http://localhost:1313/applications/smt-solver/ Theorem Prover - https://example.org/applications/theorem-prover/ + http://localhost:1313/applications/theorem-prover/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/applications/theorem-prover/ + http://localhost:1313/applications/theorem-prover/ diff --git a/applications/sat-solver/index.html b/applications/sat-solver/index.html index 4d3e9d9..3963d33 100644 --- a/applications/sat-solver/index.html +++ b/applications/sat-solver/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/sat-solver/index.xml b/applications/sat-solver/index.xml index ae89684..a04eb06 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> Glucose - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> Riss - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> Yices 2 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/applications/smt-solver/index.html b/applications/smt-solver/index.html index 8e222d1..64630b0 100644 --- a/applications/smt-solver/index.html +++ b/applications/smt-solver/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/smt-solver/index.xml b/applications/smt-solver/index.xml index dc28476..b4309c0 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> cvc4 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> Q3B - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/applications/theorem-prover/index.html b/applications/theorem-prover/index.html index e9db727..f0e5bc4 100644 --- a/applications/theorem-prover/index.html +++ b/applications/theorem-prover/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/applications/theorem-prover/index.xml b/applications/theorem-prover/index.xml index bba7549..b9e7633 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/contribute/index.html b/contribute/index.html index af98834..d96b158 100644 --- a/contribute/index.html +++ b/contribute/index.html @@ -1,6 +1,6 @@ - + @@ -13,17 +13,20 @@ - - + + - + - - - - + + + + - + @@ -65,6 +68,11 @@

Instructions coming soon. Please see https://gitmoss.fyi/fmtools/content/wiki/Contribute for temporary instructions.

+ +
diff --git a/developers/albert-ludwigs-universität/index.html b/developers/albert-ludwigs-universität/index.html index 5adca3f..aa7f901 100644 --- a/developers/albert-ludwigs-universität/index.html +++ b/developers/albert-ludwigs-universität/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/albert-ludwigs-universität/index.xml b/developers/albert-ludwigs-universität/index.xml index fa99271..1483011 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/developers/cea/index.html b/developers/cea/index.html index 9a91dd7..dd06f83 100644 --- a/developers/cea/index.html +++ b/developers/cea/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/cea/index.xml b/developers/cea/index.xml index 06e663b..ca89d51 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/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 65532f4..779f4b3 100644 --- a/developers/disi-university-of-trento/index.html +++ b/developers/disi-university-of-trento/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/disi-university-of-trento/index.xml b/developers/disi-university-of-trento/index.xml index 05790f9..55d26af 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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 f29d58e..5d5ef0f 100644 --- a/developers/eindhoven-university-of-technology/index.html +++ b/developers/eindhoven-university-of-technology/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/eindhoven-university-of-technology/index.xml b/developers/eindhoven-university-of-technology/index.xml index 9233983..96f23e7 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">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 1786b86..58b1e43 100644 --- a/developers/fondazione-bruno-kessler/index.html +++ b/developers/fondazione-bruno-kessler/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/fondazione-bruno-kessler/index.xml b/developers/fondazione-bruno-kessler/index.xml index c7231af..984bcd0 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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 b909680..037e43c 100644 --- a/developers/gilles-audemard/index.html +++ b/developers/gilles-audemard/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/gilles-audemard/index.xml b/developers/gilles-audemard/index.xml index 3c9b927..88b5611 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/developers/index.html b/developers/index.html index bad591d..1d4a13a 100644 --- a/developers/index.html +++ b/developers/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/index.xml b/developers/index.xml index 6ff8e08..5a148e2 100644 --- a/developers/index.xml +++ b/developers/index.xml @@ -2,178 +2,178 @@ Developers on Formal Methods Tools - https://example.org/developers/ + http://localhost:1313/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/ + http://localhost:1313/developers/albert-ludwigs-universit%C3%A4t/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/albert-ludwigs-universit%C3%A4t/ + http://localhost:1313/developers/albert-ludwigs-universit%C3%A4t/ CEA - https://example.org/developers/cea/ + http://localhost:1313/developers/cea/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/cea/ + http://localhost:1313/developers/cea/ DISI-University of Trento - https://example.org/developers/disi-university-of-trento/ + http://localhost:1313/developers/disi-university-of-trento/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/disi-university-of-trento/ + http://localhost:1313/developers/disi-university-of-trento/ Eindhoven University of Technology - https://example.org/developers/eindhoven-university-of-technology/ + http://localhost:1313/developers/eindhoven-university-of-technology/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/eindhoven-university-of-technology/ + http://localhost:1313/developers/eindhoven-university-of-technology/ Fondazione Bruno Kessler - https://example.org/developers/fondazione-bruno-kessler/ + http://localhost:1313/developers/fondazione-bruno-kessler/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/fondazione-bruno-kessler/ + http://localhost:1313/developers/fondazione-bruno-kessler/ Gilles Audemard - https://example.org/developers/gilles-audemard/ + http://localhost:1313/developers/gilles-audemard/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/gilles-audemard/ + http://localhost:1313/developers/gilles-audemard/ INRIA Rhône-Alpes - https://example.org/developers/inria-rh%C3%B4ne-alpes/ + http://localhost:1313/developers/inria-rh%C3%B4ne-alpes/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/inria-rh%C3%B4ne-alpes/ + http://localhost:1313/developers/inria-rh%C3%B4ne-alpes/ Johannes Kepler Universität Linz - https://example.org/developers/johannes-kepler-universit%C3%A4t-linz/ + http://localhost:1313/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/ + http://localhost:1313/developers/johannes-kepler-universit%C3%A4t-linz/ Laurent Simon - https://example.org/developers/laurent-simon/ + http://localhost:1313/developers/laurent-simon/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/laurent-simon/ + http://localhost:1313/developers/laurent-simon/ LORIA - https://example.org/developers/loria/ + http://localhost:1313/developers/loria/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/loria/ + http://localhost:1313/developers/loria/ Masaryk University - https://example.org/developers/masaryk-university/ + http://localhost:1313/developers/masaryk-university/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/masaryk-university/ + http://localhost:1313/developers/masaryk-university/ Microsoft Research - https://example.org/developers/microsoft-research/ + http://localhost:1313/developers/microsoft-research/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/microsoft-research/ + http://localhost:1313/developers/microsoft-research/ Niklas Eén - https://example.org/developers/niklas-e%C3%A9n/ + http://localhost:1313/developers/niklas-e%C3%A9n/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/niklas-e%C3%A9n/ + http://localhost:1313/developers/niklas-e%C3%A9n/ Niklas Sörensson - https://example.org/developers/niklas-s%C3%B6rensson/ + http://localhost:1313/developers/niklas-s%C3%B6rensson/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/niklas-s%C3%B6rensson/ + http://localhost:1313/developers/niklas-s%C3%B6rensson/ Norbert Manthey - https://example.org/developers/norbert-manthey/ + http://localhost:1313/developers/norbert-manthey/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/norbert-manthey/ + http://localhost:1313/developers/norbert-manthey/ RWTH Aachen - https://example.org/developers/rwth-aachen/ + http://localhost:1313/developers/rwth-aachen/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/rwth-aachen/ + http://localhost:1313/developers/rwth-aachen/ SRI International - https://example.org/developers/sri-international/ + http://localhost:1313/developers/sri-international/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/sri-international/ + http://localhost:1313/developers/sri-international/ Stanford University - https://example.org/developers/stanford-university/ + http://localhost:1313/developers/stanford-university/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/stanford-university/ + http://localhost:1313/developers/stanford-university/ ULiege - https://example.org/developers/uliege/ + http://localhost:1313/developers/uliege/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/uliege/ + http://localhost:1313/developers/uliege/ University of Freiburg - https://example.org/developers/university-of-freiburg/ + http://localhost:1313/developers/university-of-freiburg/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-freiburg/ + http://localhost:1313/developers/university-of-freiburg/ University of Illinois - https://example.org/developers/university-of-illinois/ + http://localhost:1313/developers/university-of-illinois/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-illinois/ + http://localhost:1313/developers/university-of-illinois/ University of Iowa - https://example.org/developers/university-of-iowa/ + http://localhost:1313/developers/university-of-iowa/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-iowa/ + http://localhost:1313/developers/university-of-iowa/ University of Lugano - https://example.org/developers/university-of-lugano/ + http://localhost:1313/developers/university-of-lugano/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-lugano/ + http://localhost:1313/developers/university-of-lugano/ University of Virginia - https://example.org/developers/university-of-virginia/ + http://localhost:1313/developers/university-of-virginia/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/developers/university-of-virginia/ + http://localhost:1313/developers/university-of-virginia/ diff --git a/developers/inria-rhône-alpes/index.html b/developers/inria-rhône-alpes/index.html index 73d8984..0683ead 100644 --- a/developers/inria-rhône-alpes/index.html +++ b/developers/inria-rhône-alpes/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/inria-rhône-alpes/index.xml b/developers/inria-rhône-alpes/index.xml index d1c745d..c9ab4b1 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">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 00ef7dd..908b40f 100644 --- a/developers/johannes-kepler-universität-linz/index.html +++ b/developers/johannes-kepler-universität-linz/index.html @@ -1,6 +1,6 @@ - + @@ -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 f19a512..29f890c 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/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 9c11f3f..1e658ef 100644 --- a/developers/laurent-simon/index.html +++ b/developers/laurent-simon/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/laurent-simon/index.xml b/developers/laurent-simon/index.xml index f9314b9..e48763d 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/developers/loria/index.html b/developers/loria/index.html index fed4cbf..b4b0377 100644 --- a/developers/loria/index.html +++ b/developers/loria/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/loria/index.xml b/developers/loria/index.xml index 8aa6973..4698554 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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 beb5063..cdaca46 100644 --- a/developers/masaryk-university/index.html +++ b/developers/masaryk-university/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/masaryk-university/index.xml b/developers/masaryk-university/index.xml index 2f36b3b..1f3632f 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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 29cd673..8360e17 100644 --- a/developers/microsoft-research/index.html +++ b/developers/microsoft-research/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/microsoft-research/index.xml b/developers/microsoft-research/index.xml index 7e073ce..12071fd 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">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 5eb134f..018623c 100644 --- a/developers/niklas-eén/index.html +++ b/developers/niklas-eén/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/niklas-eén/index.xml b/developers/niklas-eén/index.xml index 8cfe3df..d94811d 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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 2363d81..a4e5e20 100644 --- a/developers/niklas-sörensson/index.html +++ b/developers/niklas-sörensson/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/niklas-sörensson/index.xml b/developers/niklas-sörensson/index.xml index e387246..6cb206f 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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 f4e1c3a..787b7b0 100644 --- a/developers/norbert-manthey/index.html +++ b/developers/norbert-manthey/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/norbert-manthey/index.xml b/developers/norbert-manthey/index.xml index ab73409..ba886b5 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/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/rwth-aachen/index.html b/developers/rwth-aachen/index.html index 4cf24fb..92489e6 100644 --- a/developers/rwth-aachen/index.html +++ b/developers/rwth-aachen/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/rwth-aachen/index.xml b/developers/rwth-aachen/index.xml index 01fb0ed..aaea8cf 100644 --- a/developers/rwth-aachen/index.xml +++ b/developers/rwth-aachen/index.xml @@ -2,17 +2,17 @@ RWTH Aachen on Formal Methods Tools - https://example.org/developers/rwth-aachen/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> diff --git a/developers/sri-international/index.html b/developers/sri-international/index.html index e50ed81..f9cac0f 100644 --- a/developers/sri-international/index.html +++ b/developers/sri-international/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/sri-international/index.xml b/developers/sri-international/index.xml index ed3c296..5afe66a 100644 --- a/developers/sri-international/index.xml +++ b/developers/sri-international/index.xml @@ -2,17 +2,17 @@ SRI International on Formal Methods Tools - https://example.org/developers/sri-international/ + http://localhost:1313/developers/sri-international/ Recent content in SRI International on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Yices 2 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> diff --git a/developers/stanford-university/index.html b/developers/stanford-university/index.html index 8aa08d9..8b3dd11 100644 --- a/developers/stanford-university/index.html +++ b/developers/stanford-university/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/stanford-university/index.xml b/developers/stanford-university/index.xml index 6b7553b..b20a48d 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> diff --git a/developers/uliege/index.html b/developers/uliege/index.html index 02a3212..7fe3b82 100644 --- a/developers/uliege/index.html +++ b/developers/uliege/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/uliege/index.xml b/developers/uliege/index.xml index cd3ac19..3d157e8 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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 955966d..8675e1e 100644 --- a/developers/university-of-freiburg/index.html +++ b/developers/university-of-freiburg/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-freiburg/index.xml b/developers/university-of-freiburg/index.xml index 2880da0..353d980 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> diff --git a/developers/university-of-illinois/index.html b/developers/university-of-illinois/index.html index 202ff36..0a83837 100644 --- a/developers/university-of-illinois/index.html +++ b/developers/university-of-illinois/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-illinois/index.xml b/developers/university-of-illinois/index.xml index cd7aade..f750089 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> diff --git a/developers/university-of-iowa/index.html b/developers/university-of-iowa/index.html index 463bf33..154df16 100644 --- a/developers/university-of-iowa/index.html +++ b/developers/university-of-iowa/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-iowa/index.xml b/developers/university-of-iowa/index.xml index 04ad907..6ee7af5 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/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 923fff8..c9d8562 100644 --- a/developers/university-of-lugano/index.html +++ b/developers/university-of-lugano/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-lugano/index.xml b/developers/university-of-lugano/index.xml index 62c4f66..4201854 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/ + http://localhost:1313/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/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> diff --git a/developers/university-of-virginia/index.html b/developers/university-of-virginia/index.html index 7025330..c9f53a2 100644 --- a/developers/university-of-virginia/index.html +++ b/developers/university-of-virginia/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/developers/university-of-virginia/index.xml b/developers/university-of-virginia/index.xml index b5ff199..93300c2 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> diff --git a/domains/index.html b/domains/index.html index 36c762b..5facfa7 100644 --- a/domains/index.html +++ b/domains/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/domains/index.xml b/domains/index.xml index b960c67..b61f720 100644 --- a/domains/index.xml +++ b/domains/index.xml @@ -2,10 +2,10 @@ Domains on Formal Methods Tools - https://example.org/domains/ + http://localhost:1313/domains/ Recent content in Domains on Formal Methods Tools Hugo en-us - + diff --git a/index.html b/index.html index 85a6002..d885295 100644 --- a/index.html +++ b/index.html @@ -1,7 +1,7 @@ - + @@ -15,16 +15,16 @@ - + - + - - - - + + + + - + @@ -95,15 +95,25 @@ Contribute

- SMT-RAT + Bitwuzla - SMT Toolbox + SMT Solver

-

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

- SMT-RAT +

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

+ Bitwuzla +
+ +
+

+ Colibri + + SMT Solver + +

+

Colibri is an SMT solver. +

+ Colibri
@@ -118,6 +128,51 @@ C++ API: …

cvc5
+
+

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

+ Q3B + + SMT Solver + +

+

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

+ Q3B +
+ +
+

+ MiniSat + + SAT Solver + +

+

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

+ MiniSat +
+ +
+

+ Boolector + + SMT Solver + +

+

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

+ Boolector +
+

MathSAT @@ -131,24 +186,48 @@ C++ API: …

- dReal + SMTInterpol - SMT Solver + Interpolating SMT Solver

-

[ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as …

- dReal +

SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. +APIs and Bindings This tool is …

+ SMTInterpol

- Yices 2 + ParaFROST SMT Solver

-

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

- Yices 2 +

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

+ ParaFROST +
+ +
+

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

+ Z3 + + Theorem Prover + +

+

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

+ Z3
@@ -163,28 +242,6 @@ C++ API: …

cvc4
-
-

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

- ParaFROST - - SMT Solver - -

-

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

- ParaFROST -
-

Lingeling @@ -197,6 +254,18 @@ C++ API: …

Lingeling

+
+

+ STP + + Simple Theorem Prover + +

+

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

+ STP +
+

Glucose @@ -221,39 +290,6 @@ C++ API: …

Riss

-
-

- Boolector - - SMT Solver - -

-

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

- Boolector -
- -
-

- MiniSat - - SAT Solver - -

-

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

- MiniSat -
- -
-

- Bitwuzla - - SMT Solver - -

-

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

- Bitwuzla -
-

CryptoMiniSat @@ -269,61 +305,26 @@ C++ Namespace: …

- SMTInterpol - - Interpolating SMT Solver - -

-

SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. -APIs and Bindings This tool is …

- SMTInterpol -
- -
-

- OpenSMT + dReal 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 +

[ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as …

+ dReal

- Z3 + SMT-RAT - Theorem Prover + SMT Toolbox

-

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

- Z3 -
- -
-

- STP - - Simple Theorem Prover - -

-

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

- STP -
- -
-

- Q3B - - SMT Solver - -

-

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

- Q3B +

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

+ SMT-RAT
diff --git a/index.xml b/index.xml index 0191d72..ea3c610 100644 --- a/index.xml +++ b/index.xml @@ -2,185 +2,185 @@ The Ultimate Formal Methods Toolbox on Formal Methods Tools - https://example.org/ + http://localhost:1313/ 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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> cvc4 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> Q3B - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> About - https://example.org/about/ + http://localhost:1313/about/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/about/ + http://localhost:1313/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/ + http://localhost:1313/contribute/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/contribute/ - <p>Instructions coming soon. Please see <a href="https://gitmoss.fyi/fmtools/content/wiki/Contribute">https://gitmoss.fyi/fmtools/content/wiki/Contribute</a> for temporary instructions.</p> + http://localhost:1313/contribute/ + <p>Instructions coming soon. Please see <a href="https://gitmoss.fyi/fmtools/content/wiki/Contribute">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">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">Submit Git Issue</a></li> </ul> MIT License - https://example.org/license/ + http://localhost:1313/license/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/license/ + http://localhost:1313/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/ + http://localhost:1313/privacy/ Mon, 01 Jan 0001 00:00:00 +0000 - https://example.org/privacy/ + http://localhost:1313/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 3e25693..864fba7 100644 --- a/inputs/cnf/index.html +++ b/inputs/cnf/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/cnf/index.xml b/inputs/cnf/index.xml index 7bde3b5..770689f 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> Glucose - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/inputs/dimacs/index.html b/inputs/dimacs/index.html index 6f6372a..cb1b20e 100644 --- a/inputs/dimacs/index.html +++ b/inputs/dimacs/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/dimacs/index.xml b/inputs/dimacs/index.xml index d72aacd..953a91d 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/inputs/index.html b/inputs/index.html index b24e977..a6ec1b6 100644 --- a/inputs/index.html +++ b/inputs/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/index.xml b/inputs/index.xml index 79edebf..d5f9346 100644 --- a/inputs/index.xml +++ b/inputs/index.xml @@ -2,38 +2,38 @@ Inputs on Formal Methods Tools - https://example.org/inputs/ + http://localhost:1313/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/ + http://localhost:1313/inputs/cnf/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/cnf/ + http://localhost:1313/inputs/cnf/ DIMACS - https://example.org/inputs/dimacs/ + http://localhost:1313/inputs/dimacs/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/dimacs/ + http://localhost:1313/inputs/dimacs/ SMTLIB2 - https://example.org/inputs/smtlib2/ + http://localhost:1313/inputs/smtlib2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/smtlib2/ + http://localhost:1313/inputs/smtlib2/ Yices 2 - https://example.org/inputs/yices-2/ + http://localhost:1313/inputs/yices-2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/inputs/yices-2/ + http://localhost:1313/inputs/yices-2/ diff --git a/inputs/smtlib2/index.html b/inputs/smtlib2/index.html index 878be45..7aa694c 100644 --- a/inputs/smtlib2/index.html +++ b/inputs/smtlib2/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/smtlib2/index.xml b/inputs/smtlib2/index.xml index e864f40..146922c 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> cvc4 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> OpenSMT - https://example.org/tools/sat-smt/opensmt/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> Q3B - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/inputs/yices-2/index.html b/inputs/yices-2/index.html index e2a78cc..6b85c17 100644 --- a/inputs/yices-2/index.html +++ b/inputs/yices-2/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/inputs/yices-2/index.xml b/inputs/yices-2/index.xml index cae8333..1f2fcc9 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> diff --git a/interfaces/.net/index.html b/interfaces/.net/index.html index 95f7211..8aec1d9 100644 --- a/interfaces/.net/index.html +++ b/interfaces/.net/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/.net/index.xml b/interfaces/.net/index.xml index 46605d7..ae91426 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/c++/index.html b/interfaces/c++/index.html index 93eaee6..b70094d 100644 --- a/interfaces/c++/index.html +++ b/interfaces/c++/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/c++/index.xml b/interfaces/c++/index.xml index ffe6a18..f0d0bbe 100644 --- a/interfaces/c++/index.xml +++ b/interfaces/c++/index.xml @@ -2,31 +2,31 @@ C++ on Formal Methods Tools - https://example.org/interfaces/c++/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/c/index.html b/interfaces/c/index.html index a155bf7..5c6f115 100644 --- a/interfaces/c/index.html +++ b/interfaces/c/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/c/index.xml b/interfaces/c/index.xml index 6e505e4..959814a 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/cli/index.html b/interfaces/cli/index.html index cf83d8b..7fdb817 100644 --- a/interfaces/cli/index.html +++ b/interfaces/cli/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/cli/index.xml b/interfaces/cli/index.xml index c2c2e0e..fc6f92b 100644 --- a/interfaces/cli/index.xml +++ b/interfaces/cli/index.xml @@ -2,157 +2,157 @@ CLI on Formal Methods Tools - https://example.org/interfaces/cli/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> cvc4 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> Q3B - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/index.html b/interfaces/index.html index e880af3..e5db271 100644 --- a/interfaces/index.html +++ b/interfaces/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/index.xml b/interfaces/index.xml index 94d4565..43838fd 100644 --- a/interfaces/index.xml +++ b/interfaces/index.xml @@ -2,66 +2,66 @@ Interfaces on Formal Methods Tools - https://example.org/interfaces/ + http://localhost:1313/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/ + http://localhost:1313/interfaces/.net/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/.net/ + http://localhost:1313/interfaces/.net/ C - https://example.org/interfaces/c/ + http://localhost:1313/interfaces/c/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/c/ + http://localhost:1313/interfaces/c/ C++ - https://example.org/interfaces/c++/ + http://localhost:1313/interfaces/c++/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/c++/ + http://localhost:1313/interfaces/c++/ CLI - https://example.org/interfaces/cli/ + http://localhost:1313/interfaces/cli/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/cli/ + http://localhost:1313/interfaces/cli/ Java - https://example.org/interfaces/java/ + http://localhost:1313/interfaces/java/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/java/ + http://localhost:1313/interfaces/java/ Online - https://example.org/interfaces/online/ + http://localhost:1313/interfaces/online/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/online/ + http://localhost:1313/interfaces/online/ Python - https://example.org/interfaces/python/ + http://localhost:1313/interfaces/python/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/python/ + http://localhost:1313/interfaces/python/ Rust - https://example.org/interfaces/rust/ + http://localhost:1313/interfaces/rust/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/interfaces/rust/ + http://localhost:1313/interfaces/rust/ diff --git a/interfaces/java/index.html b/interfaces/java/index.html index 3319a91..59406b5 100644 --- a/interfaces/java/index.html +++ b/interfaces/java/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/java/index.xml b/interfaces/java/index.xml index f83e419..9e788b5 100644 --- a/interfaces/java/index.xml +++ b/interfaces/java/index.xml @@ -2,24 +2,24 @@ Java on Formal Methods Tools - https://example.org/interfaces/java/ + http://localhost:1313/interfaces/java/ Recent content in Java on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/online/index.html b/interfaces/online/index.html index 3d19eaa..e7d0a41 100644 --- a/interfaces/online/index.html +++ b/interfaces/online/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/online/index.xml b/interfaces/online/index.xml index b79c910..05cc60a 100644 --- a/interfaces/online/index.xml +++ b/interfaces/online/index.xml @@ -2,31 +2,31 @@ Online on Formal Methods Tools - https://example.org/interfaces/online/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/python/index.html b/interfaces/python/index.html index 00c35ee..2b48c89 100644 --- a/interfaces/python/index.html +++ b/interfaces/python/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/python/index.xml b/interfaces/python/index.xml index e8ecb79..9eea7e9 100644 --- a/interfaces/python/index.xml +++ b/interfaces/python/index.xml @@ -2,38 +2,38 @@ Python on Formal Methods Tools - https://example.org/interfaces/python/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> Yices 2 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/interfaces/rust/index.html b/interfaces/rust/index.html index d200ca4..1e37db4 100644 --- a/interfaces/rust/index.html +++ b/interfaces/rust/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/interfaces/rust/index.xml b/interfaces/rust/index.xml index 213723f..4900c38 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/license/index.html b/license/index.html index d961d2a..ad1f6a4 100644 --- a/license/index.html +++ b/license/index.html @@ -1,6 +1,6 @@ - + @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/all-rights-reserved/index.html b/licenses/all-rights-reserved/index.html index 8833069..cee9b57 100644 --- a/licenses/all-rights-reserved/index.html +++ b/licenses/all-rights-reserved/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/all-rights-reserved/index.xml b/licenses/all-rights-reserved/index.xml index ef314b9..6b4727e 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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 09025d6..2d0ca85 100644 --- a/licenses/apache-2.0/index.html +++ b/licenses/apache-2.0/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/apache-2.0/index.xml b/licenses/apache-2.0/index.xml index b9ed02c..1a3c993 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/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 ddb1a22..5a42f79 100644 --- a/licenses/bsd/index.html +++ b/licenses/bsd/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/bsd/index.xml b/licenses/bsd/index.xml index 81b447d..2f7c887 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> veriT - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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 5cf83a7..1ef3327 100644 --- a/licenses/gplv2/index.html +++ b/licenses/gplv2/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/gplv2/index.xml b/licenses/gplv2/index.xml index 84b6a06..4792347 100644 --- a/licenses/gplv2/index.xml +++ b/licenses/gplv2/index.xml @@ -2,17 +2,17 @@ GPLv2 on Formal Methods Tools - https://example.org/licenses/gplv2/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> diff --git a/licenses/gplv3/index.html b/licenses/gplv3/index.html index 153a34b..0b1fb34 100644 --- a/licenses/gplv3/index.html +++ b/licenses/gplv3/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/gplv3/index.xml b/licenses/gplv3/index.xml index c79d1b7..bd8233f 100644 --- a/licenses/gplv3/index.xml +++ b/licenses/gplv3/index.xml @@ -2,38 +2,38 @@ GPLv3 on Formal Methods Tools - https://example.org/licenses/gplv3/ + http://localhost:1313/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/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> Yices 2 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> diff --git a/licenses/index.html b/licenses/index.html index 60b1dec..127094c 100644 --- a/licenses/index.html +++ b/licenses/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/index.xml b/licenses/index.xml index b5a643e..caa8fad 100644 --- a/licenses/index.xml +++ b/licenses/index.xml @@ -2,59 +2,59 @@ Licenses on Formal Methods Tools - https://example.org/licenses/ + http://localhost:1313/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/ + http://localhost:1313/licenses/all-rights-reserved/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/all-rights-reserved/ + http://localhost:1313/licenses/all-rights-reserved/ Apache-2.0 - https://example.org/licenses/apache-2.0/ + http://localhost:1313/licenses/apache-2.0/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/apache-2.0/ + http://localhost:1313/licenses/apache-2.0/ BSD - https://example.org/licenses/bsd/ + http://localhost:1313/licenses/bsd/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/bsd/ + http://localhost:1313/licenses/bsd/ GPLv2 - https://example.org/licenses/gplv2/ + http://localhost:1313/licenses/gplv2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/gplv2/ + http://localhost:1313/licenses/gplv2/ GPLv3 - https://example.org/licenses/gplv3/ + http://localhost:1313/licenses/gplv3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/gplv3/ + http://localhost:1313/licenses/gplv3/ LGPLv2 - https://example.org/licenses/lgplv2/ + http://localhost:1313/licenses/lgplv2/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/lgplv2/ + http://localhost:1313/licenses/lgplv2/ MIT - https://example.org/licenses/mit/ + http://localhost:1313/licenses/mit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/licenses/mit/ + http://localhost:1313/licenses/mit/ diff --git a/licenses/lgplv2/index.html b/licenses/lgplv2/index.html index e8db894..39623a6 100644 --- a/licenses/lgplv2/index.html +++ b/licenses/lgplv2/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/lgplv2/index.xml b/licenses/lgplv2/index.xml index 8991086..9663160 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/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 a655ccf..ba546dc 100644 --- a/licenses/mit/index.html +++ b/licenses/mit/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/licenses/mit/index.xml b/licenses/mit/index.xml index 35a6764..38a477f 100644 --- a/licenses/mit/index.xml +++ b/licenses/mit/index.xml @@ -2,87 +2,87 @@ MIT on Formal Methods Tools - https://example.org/licenses/mit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> Glucose - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MiniSat - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/maintenance/actively-maintained/index.html b/maintenance/actively-maintained/index.html index 3ec8255..da2508a 100644 --- a/maintenance/actively-maintained/index.html +++ b/maintenance/actively-maintained/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/maintenance/actively-maintained/index.xml b/maintenance/actively-maintained/index.xml index e51ca6a..95fc23b 100644 --- a/maintenance/actively-maintained/index.xml +++ b/maintenance/actively-maintained/index.xml @@ -2,115 +2,115 @@ Actively Maintained on Formal Methods Tools - https://example.org/maintenance/actively-maintained/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> cvc5 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> Glucose - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> SMT-RAT - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/maintenance/index.html b/maintenance/index.html index 4d83433..9526c94 100644 --- a/maintenance/index.html +++ b/maintenance/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/maintenance/index.xml b/maintenance/index.xml index b99557d..110dd90 100644 --- a/maintenance/index.xml +++ b/maintenance/index.xml @@ -2,24 +2,24 @@ Maintenance on Formal Methods Tools - https://example.org/maintenance/ + http://localhost:1313/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/ + http://localhost:1313/maintenance/actively-maintained/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/maintenance/actively-maintained/ + http://localhost:1313/maintenance/actively-maintained/ Not Maintained - https://example.org/maintenance/not-maintained/ + http://localhost:1313/maintenance/not-maintained/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/maintenance/not-maintained/ + http://localhost:1313/maintenance/not-maintained/ diff --git a/maintenance/not-maintained/index.html b/maintenance/not-maintained/index.html index d0f7a7d..eb27346 100644 --- a/maintenance/not-maintained/index.html +++ b/maintenance/not-maintained/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/maintenance/not-maintained/index.xml b/maintenance/not-maintained/index.xml index 635b8da..01535bc 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/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 d67473e..8e39e5e 100644 --- a/privacy/index.html +++ b/privacy/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/sitemap.xml b/sitemap.xml index 0388399..ee764f7 100644 --- a/sitemap.xml +++ b/sitemap.xml @@ -2,268 +2,268 @@ - https://example.org/interfaces/.net/ + http://localhost:1313/interfaces/.net/ 2025-06-07T00:00:00+00:00 - https://example.org/maintenance/actively-maintained/ + http://localhost:1313/maintenance/actively-maintained/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/albert-ludwigs-universit%C3%A4t/ + http://localhost:1313/developers/albert-ludwigs-universit%C3%A4t/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/pmc/ + http://localhost:1313/tools/pmc/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/all-rights-reserved/ + http://localhost:1313/licenses/all-rights-reserved/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/ + http://localhost:1313/tools/sat-smt/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/termination/ + http://localhost:1313/tools/termination/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/ + http://localhost:1313/tools/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/apache-2.0/ + http://localhost:1313/licenses/apache-2.0/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/ + http://localhost:1313/applications/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/tools/sat-smt/bitwuzla/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/tools/sat-smt/boolector/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/bsd/ + http://localhost:1313/licenses/bsd/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/c/ + http://localhost:1313/interfaces/c/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/c++/ + http://localhost:1313/interfaces/c++/ 2025-06-07T00:00:00+00:00 - https://example.org/techniques/cdcl/ + http://localhost:1313/techniques/cdcl/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/cea/ + http://localhost:1313/developers/cea/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/cli/ + http://localhost:1313/interfaces/cli/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/cnf/ + http://localhost:1313/inputs/cnf/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/constraint-solver/ + http://localhost:1313/applications/constraint-solver/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/tools/sat-smt/cryptominisat/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/tools/sat-smt/cvc4/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/ + http://localhost:1313/developers/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/dimacs/ + http://localhost:1313/inputs/dimacs/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/disi-university-of-trento/ + http://localhost:1313/developers/disi-university-of-trento/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/tools/sat-smt/dreal/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/eindhoven-university-of-technology/ + http://localhost:1313/developers/eindhoven-university-of-technology/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/fondazione-bruno-kessler/ + http://localhost:1313/developers/fondazione-bruno-kessler/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/gilles-audemard/ + http://localhost:1313/developers/gilles-audemard/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/gplv2/ + http://localhost:1313/licenses/gplv2/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/gplv3/ + http://localhost:1313/licenses/gplv3/ 2025-06-07T00:00:00+00:00 - https://example.org/techniques/gpu/ + http://localhost:1313/techniques/gpu/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/ + http://localhost:1313/inputs/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/inria-rh%C3%B4ne-alpes/ + http://localhost:1313/developers/inria-rh%C3%B4ne-alpes/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/ + http://localhost:1313/interfaces/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/java/ + http://localhost:1313/interfaces/java/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/johannes-kepler-universit%C3%A4t-linz/ + http://localhost:1313/developers/johannes-kepler-universit%C3%A4t-linz/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/laurent-simon/ + http://localhost:1313/developers/laurent-simon/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/lgplv2/ + http://localhost:1313/licenses/lgplv2/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/ + http://localhost:1313/licenses/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/loria/ + http://localhost:1313/developers/loria/ 2025-06-07T00:00:00+00:00 - https://example.org/maintenance/ + http://localhost:1313/maintenance/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/masaryk-university/ + http://localhost:1313/developers/masaryk-university/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/tools/sat-smt/mathsat/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/microsoft-research/ + http://localhost:1313/developers/microsoft-research/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/tools/sat-smt/minisat/ 2025-06-07T00:00:00+00:00 - https://example.org/licenses/mit/ + http://localhost:1313/licenses/mit/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/niklas-e%C3%A9n/ + http://localhost:1313/developers/niklas-e%C3%A9n/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/niklas-s%C3%B6rensson/ + http://localhost:1313/developers/niklas-s%C3%B6rensson/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/norbert-manthey/ + http://localhost:1313/developers/norbert-manthey/ 2025-06-07T00:00:00+00:00 - https://example.org/maintenance/not-maintained/ + http://localhost:1313/maintenance/not-maintained/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/online/ + http://localhost:1313/interfaces/online/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/opensmt/ + http://localhost:1313/tools/sat-smt/opensmt/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/tools/sat-smt/parafrost/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/python/ + http://localhost:1313/interfaces/python/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/tools/sat-smt/q3b/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/tools/sat-smt/riss/ 2025-06-07T00:00:00+00:00 - https://example.org/interfaces/rust/ + http://localhost:1313/interfaces/rust/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/rwth-aachen/ + http://localhost:1313/developers/rwth-aachen/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/sat-solver/ + http://localhost:1313/applications/sat-solver/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/smt-solver/ + http://localhost:1313/applications/smt-solver/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/tools/sat-smt/smt-rat/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/smtlib2/ + http://localhost:1313/inputs/smtlib2/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/sri-international/ + http://localhost:1313/developers/sri-international/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/stanford-university/ + http://localhost:1313/developers/stanford-university/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ 2025-06-07T00:00:00+00:00 - https://example.org/techniques/ + http://localhost:1313/techniques/ 2025-06-07T00:00:00+00:00 - https://example.org/ + http://localhost:1313/ 2025-06-07T00:00:00+00:00 - https://example.org/applications/theorem-prover/ + http://localhost:1313/applications/theorem-prover/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/uliege/ + http://localhost:1313/developers/uliege/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-freiburg/ + http://localhost:1313/developers/university-of-freiburg/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-illinois/ + http://localhost:1313/developers/university-of-illinois/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-iowa/ + http://localhost:1313/developers/university-of-iowa/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-lugano/ + http://localhost:1313/developers/university-of-lugano/ 2025-06-07T00:00:00+00:00 - https://example.org/developers/university-of-virginia/ + http://localhost:1313/developers/university-of-virginia/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ 2025-06-07T00:00:00+00:00 - https://example.org/inputs/yices-2/ + http://localhost:1313/inputs/yices-2/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/tools/sat-smt/yices/ 2025-06-07T00:00:00+00:00 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ 2025-06-07T00:00:00+00:00 - https://example.org/about/ + http://localhost:1313/about/ - https://example.org/taxonomies/ + http://localhost:1313/taxonomies/ - https://example.org/contribute/ + http://localhost:1313/contribute/ - https://example.org/domains/ + http://localhost:1313/domains/ - https://example.org/license/ + http://localhost:1313/license/ - https://example.org/privacy/ + http://localhost:1313/privacy/ diff --git a/taxonomies/index.html b/taxonomies/index.html index 1b52e0d..700c9c3 100644 --- a/taxonomies/index.html +++ b/taxonomies/index.html @@ -1,6 +1,6 @@ - + @@ -15,16 +15,16 @@ - + - + - - - - + + + + - + diff --git a/taxonomies/index.xml b/taxonomies/index.xml index 19d5fe8..02bdae5 100644 --- a/taxonomies/index.xml +++ b/taxonomies/index.xml @@ -2,10 +2,10 @@ All Taxonomy Data on Formal Methods Tools - https://example.org/taxonomies/ + http://localhost:1313/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 a5a77cf..cc1cb94 100644 --- a/techniques/cdcl/index.html +++ b/techniques/cdcl/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/techniques/cdcl/index.xml b/techniques/cdcl/index.xml index 8f1909f..04d5c19 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/techniques/gpu/index.html b/techniques/gpu/index.html index 6fea698..0746062 100644 --- a/techniques/gpu/index.html +++ b/techniques/gpu/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/techniques/gpu/index.xml b/techniques/gpu/index.xml index 5d52b2e..4b8744f 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/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> diff --git a/techniques/index.html b/techniques/index.html index 1e74fa0..ca1b363 100644 --- a/techniques/index.html +++ b/techniques/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/techniques/index.xml b/techniques/index.xml index 92394f1..393379d 100644 --- a/techniques/index.xml +++ b/techniques/index.xml @@ -2,24 +2,24 @@ Techniques on Formal Methods Tools - https://example.org/techniques/ + http://localhost:1313/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/ + http://localhost:1313/techniques/cdcl/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/techniques/cdcl/ + http://localhost:1313/techniques/cdcl/ GPU - https://example.org/techniques/gpu/ + http://localhost:1313/techniques/gpu/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/techniques/gpu/ + http://localhost:1313/techniques/gpu/ diff --git a/tools/index.html b/tools/index.html index 18c4566..8941098 100644 --- a/tools/index.html +++ b/tools/index.html @@ -1,6 +1,6 @@ - + @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + @@ -65,53 +65,53 @@ Click a colorful item in the"> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/tools/index.xml b/tools/index.xml index 8c61c25..b91a5bd 100644 --- a/tools/index.xml +++ b/tools/index.xml @@ -2,11 +2,11 @@ All Tools on Formal Methods Tools - https://example.org/tools/ + http://localhost:1313/tools/ Recent content in All Tools on Formal Methods Tools Hugo en-us - + diff --git a/tools/pmc/index.html b/tools/pmc/index.html index ca95d8b..d076a50 100644 --- a/tools/pmc/index.html +++ b/tools/pmc/index.html @@ -1,6 +1,6 @@ - + @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/pmc/index.xml b/tools/pmc/index.xml index cd8230d..13d30ce 100644 --- a/tools/pmc/index.xml +++ b/tools/pmc/index.xml @@ -2,11 +2,11 @@ All PMC Tools on Formal Methods Tools - https://example.org/tools/pmc/ + http://localhost:1313/tools/pmc/ Recent content in All PMC Tools on Formal Methods Tools Hugo en-us - + diff --git a/tools/sat-smt/bitwuzla/index.html b/tools/sat-smt/bitwuzla/index.html index f4c2647..5a83b04 100644 --- a/tools/sat-smt/bitwuzla/index.html +++ b/tools/sat-smt/bitwuzla/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -428,7 +428,9 @@
Help improve this page!
- Submit an issue or pull request. + Submit an + issue or + pull request.
diff --git a/tools/sat-smt/boolector/index.html b/tools/sat-smt/boolector/index.html index 4e2f9a4..e9d2e7c 100644 --- a/tools/sat-smt/boolector/index.html +++ b/tools/sat-smt/boolector/index.html @@ -1,6 +1,6 @@ - + @@ -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 847bf67..954e25d 100644 --- a/tools/sat-smt/colibri/index.html +++ b/tools/sat-smt/colibri/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/cryptominisat/index.html b/tools/sat-smt/cryptominisat/index.html index 2ef3787..bc652af 100644 --- a/tools/sat-smt/cryptominisat/index.html +++ b/tools/sat-smt/cryptominisat/index.html @@ -1,6 +1,6 @@ - + @@ -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 cb9cd8b..279e20e 100644 --- a/tools/sat-smt/cvc4/index.html +++ b/tools/sat-smt/cvc4/index.html @@ -1,6 +1,6 @@ - + @@ -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 e9e9f8e..5eec4bd 100644 --- a/tools/sat-smt/cvc5/index.html +++ b/tools/sat-smt/cvc5/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/dreal/index.html b/tools/sat-smt/dreal/index.html index 9741f27..1a175b7 100644 --- a/tools/sat-smt/dreal/index.html +++ b/tools/sat-smt/dreal/index.html @@ -1,6 +1,6 @@ - + @@ -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 3e4a64c..525fc78 100644 --- a/tools/sat-smt/glucose/index.html +++ b/tools/sat-smt/glucose/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/index.html b/tools/sat-smt/index.html index 0ded095..78bd812 100644 --- a/tools/sat-smt/index.html +++ b/tools/sat-smt/index.html @@ -1,6 +1,6 @@ - + @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/index.xml b/tools/sat-smt/index.xml index 33dfe44..481b625 100644 --- a/tools/sat-smt/index.xml +++ b/tools/sat-smt/index.xml @@ -2,157 +2,157 @@ All SAT & SMT Tools on Formal Methods Tools - https://example.org/tools/sat-smt/ + http://localhost:1313/tools/sat-smt/ Recent content in All 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/ + http://localhost:1313/tools/sat-smt/bitwuzla/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/bitwuzla/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/boolector/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/colibri/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/colibri/ + http://localhost:1313/tools/sat-smt/colibri/ <p>Colibri is an SMT solver.</p> CryptoMiniSat - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/tools/sat-smt/cryptominisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cryptominisat/ + http://localhost:1313/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/">homepage</a></li> <li><strong>Python package:</strong> <a href="https://pypi.org/project/pycryptosat/">PyPI package</a></li> </ul> cvc4 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/tools/sat-smt/cvc4/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc4/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/cvc5/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/cvc5/ + http://localhost:1313/tools/sat-smt/cvc5/ <p>cvc5 is an automatic theorem prover for SMT problems.</p> dReal - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/tools/sat-smt/dreal/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/dreal/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/glucose/ + http://localhost:1313/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/lingeling/ + http://localhost:1313/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/mathsat/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/minisat/ + http://localhost:1313/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/ + http://localhost:1313/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> + http://localhost:1313/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="http://localhost:1313/tools/minisat">MiniSAT</a>.</p> ParaFROST - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/parafrost/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li> </ul> Q3B - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/q3b/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/riss/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smt-rat/ + http://localhost:1313/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">C++ API Reference</a></li> </ul> SMTInterpol - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/smtinterpol/ + http://localhost:1313/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">Java API Reference</a></li> </ul> STP - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/stp/ + http://localhost:1313/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">stp C API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li> </ul> veriT - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/verit/ + http://localhost:1313/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/ + http://localhost:1313/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/yices/ + http://localhost:1313/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">Yices API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li> </ul> Z3 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - https://example.org/tools/sat-smt/z3/ + http://localhost:1313/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">Z3 C API Reference</a></li> <li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">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">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">Z3 Java API Reference</a></li> <li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li> <li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">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 4afd6bf..2582979 100644 --- a/tools/sat-smt/lingeling/index.html +++ b/tools/sat-smt/lingeling/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/mathsat/index.html b/tools/sat-smt/mathsat/index.html index e6e56eb..6f07045 100644 --- a/tools/sat-smt/mathsat/index.html +++ b/tools/sat-smt/mathsat/index.html @@ -1,6 +1,6 @@ - + @@ -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 57eebc6..0994631 100644 --- a/tools/sat-smt/minisat/index.html +++ b/tools/sat-smt/minisat/index.html @@ -1,6 +1,6 @@ - + @@ -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 c8150d3..ffd27a3 100644 --- a/tools/sat-smt/opensmt/index.html +++ b/tools/sat-smt/opensmt/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/parafrost/index.html b/tools/sat-smt/parafrost/index.html index d31c819..98439b6 100644 --- a/tools/sat-smt/parafrost/index.html +++ b/tools/sat-smt/parafrost/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/q3b/index.html b/tools/sat-smt/q3b/index.html index 7f6e6ce..8f7491c 100644 --- a/tools/sat-smt/q3b/index.html +++ b/tools/sat-smt/q3b/index.html @@ -1,6 +1,6 @@ - + @@ -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 568b259..e5ef9e9 100644 --- a/tools/sat-smt/riss/index.html +++ b/tools/sat-smt/riss/index.html @@ -1,6 +1,6 @@ - + @@ -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 f23531b..9c00e8e 100644 --- a/tools/sat-smt/smt-rat/index.html +++ b/tools/sat-smt/smt-rat/index.html @@ -1,6 +1,6 @@ - + @@ -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 9b079a9..a73e20f 100644 --- a/tools/sat-smt/smtinterpol/index.html +++ b/tools/sat-smt/smtinterpol/index.html @@ -1,6 +1,6 @@ - + @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/stp/index.html b/tools/sat-smt/stp/index.html index 1412651..3f089c9 100644 --- a/tools/sat-smt/stp/index.html +++ b/tools/sat-smt/stp/index.html @@ -1,6 +1,6 @@ - + @@ -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 0e53540..f04b3a9 100644 --- a/tools/sat-smt/verit/index.html +++ b/tools/sat-smt/verit/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/yices/index.html b/tools/sat-smt/yices/index.html index 7bd921e..a487d14 100644 --- a/tools/sat-smt/yices/index.html +++ b/tools/sat-smt/yices/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/tools/sat-smt/z3/index.html b/tools/sat-smt/z3/index.html index 1d3ff74..abeb762 100644 --- a/tools/sat-smt/z3/index.html +++ b/tools/sat-smt/z3/index.html @@ -1,6 +1,6 @@ - + @@ -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 07ec875..37df75c 100644 --- a/tools/termination/index.html +++ b/tools/termination/index.html @@ -1,6 +1,6 @@ - + @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + diff --git a/tools/termination/index.xml b/tools/termination/index.xml index 525169f..b41735c 100644 --- a/tools/termination/index.xml +++ b/tools/termination/index.xml @@ -2,11 +2,11 @@ All Termination Tools on Formal Methods Tools - https://example.org/tools/termination/ + http://localhost:1313/tools/termination/ Recent content in All Termination Tools on Formal Methods Tools Hugo en-us - +