diff --git a/404.html b/404.html index 539cb1d..79c23dc 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 43d0164..569b551 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 7f448f0..fd26f5a 100644 --- a/applications/constraint-solver/index.html +++ b/applications/constraint-solver/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … diff --git a/applications/constraint-solver/index.xml b/applications/constraint-solver/index.xml index cad232f..fd169a4 100644 --- a/applications/constraint-solver/index.xml +++ b/applications/constraint-solver/index.xml @@ -2,17 +2,17 @@ Constraint Solver on Formal Methods Tools - http://localhost:1313/applications/constraint-solver/ + https://example.org/applications/constraint-solver/ Recent content in Constraint Solver on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + STP - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 4edaff0..f14fa96 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 56f8230..4132ce0 100644 --- a/applications/index.xml +++ b/applications/index.xml @@ -2,38 +2,38 @@ Applications on Formal Methods Tools - http://localhost:1313/applications/ + https://example.org/applications/ Recent content in Applications on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Constraint Solver - http://localhost:1313/applications/constraint-solver/ + https://example.org/applications/constraint-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/applications/constraint-solver/ + https://example.org/applications/constraint-solver/ SAT Solver - http://localhost:1313/applications/sat-solver/ + https://example.org/applications/sat-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/applications/sat-solver/ + https://example.org/applications/sat-solver/ SMT Solver - http://localhost:1313/applications/smt-solver/ + https://example.org/applications/smt-solver/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/applications/smt-solver/ + https://example.org/applications/smt-solver/ Theorem Prover - http://localhost:1313/applications/theorem-prover/ + https://example.org/applications/theorem-prover/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/applications/theorem-prover/ + https://example.org/applications/theorem-prover/ diff --git a/applications/sat-solver/index.html b/applications/sat-solver/index.html index 62321d5..4d3e9d9 100644 --- a/applications/sat-solver/index.html +++ b/applications/sat-solver/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,16 +81,67 @@ - - ParaFROST + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … + + + + + + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … + + + + + + + Glucose + Glucose is a SAT solver. + + + + + + + + Lingeling + Lingeling is a SAT solver. + + + + + + + + MiniSat + [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … + + + + + + + ParaFROST ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … - - Riss + + Riss [ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. @@ -98,8 +149,8 @@ - - SMT-RAT + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … @@ -107,16 +158,16 @@ APIs and Bindings This tool is available through the … - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/applications/sat-solver/index.xml b/applications/sat-solver/index.xml index 287caf1..ae89684 100644 --- a/applications/sat-solver/index.xml +++ b/applications/sat-solver/index.xml @@ -2,45 +2,87 @@ SAT Solver on Formal Methods Tools - http://localhost:1313/applications/sat-solver/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/glucose/ + <p>Glucose is a SAT solver.</p> + + + Lingeling + https://example.org/tools/sat-smt/lingeling/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/lingeling/ + <p>Lingeling is a SAT solver.</p> + + + MiniSat + https://example.org/tools/sat-smt/minisat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/parafrost/ + https://example.org/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/parafrost/ + https://example.org/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 - http://localhost:1313/tools/riss/ + https://example.org/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/riss/ + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 3369ae3..8e222d1 100644 --- a/applications/smt-solver/index.html +++ b/applications/smt-solver/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,16 +81,82 @@ - - Q3B + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … + + + + + + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + Colibri + Colibri is an SMT solver. + + + + + + + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + dReal + [ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems … + + + + + + + MathSAT + [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … + + + + + + + OpenSMT + OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … + + + + + + + Q3B [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … - - SMT-RAT + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … @@ -98,8 +164,8 @@ APIs and Bindings This tool is available through the … - - SMTInterpol + + SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and … @@ -107,8 +173,8 @@ APIs and … - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -116,24 +182,24 @@ APIs and Bindings This tool is available … - - veriT + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/applications/smt-solver/index.xml b/applications/smt-solver/index.xml index 9120700..dc28476 100644 --- a/applications/smt-solver/index.xml +++ b/applications/smt-solver/index.xml @@ -2,59 +2,115 @@ SMT Solver on Formal Methods Tools - http://localhost:1313/applications/smt-solver/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/colibri/ + <p>Colibri is an SMT solver.</p> + + + cvc4 + https://example.org/tools/sat-smt/cvc4/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + + dReal + https://example.org/tools/sat-smt/dreal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + 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> + Q3B - http://localhost:1313/tools/q3b/ + https://example.org/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/q3b/ + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 5342884..e9db727 100644 --- a/applications/theorem-prover/index.html +++ b/applications/theorem-prover/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,41 @@ - - STP + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … + + + + + + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -90,8 +123,8 @@ APIs and Bindings This tool is available … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/applications/theorem-prover/index.xml b/applications/theorem-prover/index.xml index 4a3e2e6..bba7549 100644 --- a/applications/theorem-prover/index.xml +++ b/applications/theorem-prover/index.xml @@ -2,24 +2,52 @@ Theorem Prover on Formal Methods Tools - http://localhost:1313/applications/theorem-prover/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + STP - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 f09d505..af98834 100644 --- a/contribute/index.html +++ b/contribute/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + diff --git a/css/styles.8b49a669b444200848aa2fc88c4dc95a3d61d6c822e7ad08eecab8049173e085d2bfa16bf17fa8ec14eb95bb1f04f9a822b2fc4836b4d329140ddd03444ca0bf.css b/css/styles.8b49a669b444200848aa2fc88c4dc95a3d61d6c822e7ad08eecab8049173e085d2bfa16bf17fa8ec14eb95bb1f04f9a822b2fc4836b4d329140ddd03444ca0bf.css deleted file mode 100644 index 3f9dc9e..0000000 --- a/css/styles.8b49a669b444200848aa2fc88c4dc95a3d61d6c822e7ad08eecab8049173e085d2bfa16bf17fa8ec14eb95bb1f04f9a822b2fc4836b4d329140ddd03444ca0bf.css +++ /dev/null @@ -1,560 +0,0 @@ -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 100; - src: local("Source Sans 3 ExtraLight"), local("SourceSans3-ExtraLight"), url("/fonts/static/SourceSans3-ExtraLight.woff2") format("woff2"), url("/fonts/static/SourceSans3-ExtraLight.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 200; - src: local("Source Sans 3 ExtraLight"), local("SourceSans3-ExtraLight"), url("/fonts/static/SourceSans3-ExtraLight.woff2") format("woff2"), url("/fonts/static/SourceSans3-ExtraLight.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 300; - src: local("Source Sans 3 Light"), local("SourceSans3-Light"), url("/fonts/static/SourceSans3-Light.woff2") format("woff2"), url("/fonts/static/SourceSans3-Light.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 400; - src: local("Source Sans 3 Regular"), local("SourceSans3-Regular"), url("/fonts/static/SourceSans3-Regular.woff2") format("woff2"), url("/fonts/static/SourceSans3-Regular.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: italic; - font-display: swap; - font-weight: 400; - src: local("Source Sans 3 Italic"), local("SourceSans3-Italic"), url("/fonts/static/SourceSans3-Italic.woff2") format("woff2"), url("/fonts/static/SourceSans3-Italic.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 500; - src: local("Source Sans 3 Medium"), local("SourceSans3-Medium"), url("/fonts/static/SourceSans3-Medium.woff2") format("woff2"), url("/fonts/static/SourceSans3-Medium.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 600; - src: local("Source Sans 3 SemiBold"), local("SourceSans3-SemiBold"), url("/fonts/static/SourceSans3-SemiBold.woff2") format("woff2"), url("/fonts/static/SourceSans3-SemiBold.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 700; - src: local("Source Sans 3 Bold"), local("SourceSans3-Bold"), url("/fonts/static/SourceSans3-Bold.woff2") format("woff2"), url("/fonts/static/SourceSans3-Bold.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: italic; - font-display: swap; - font-weight: 700; - src: local("Source Sans 3 Bold Italic"), local("SourceSans3-BoldItalic"), url("/fonts/static/SourceSans3-BoldItalic.woff2") format("woff2"), url("/fonts/static/SourceSans3-BoldItalic.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 800; - src: local("Source Sans 3 ExtraBold"), local("SourceSans3-ExtraBold"), url("/fonts/static/SourceSans3-ExtraBold.woff2") format("woff2"), url("/fonts/static/SourceSans3-ExtraBold.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Sans 3'; - font-style: normal; - font-display: swap; - font-weight: 900; - src: local("Source Sans 3 Black"), local("SourceSans3-Black"), url("/fonts/static/SourceSans3-Black.woff2") format("woff2"), url("/fonts/static/SourceSans3-Black.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Code Pro'; - font-style: normal; - font-display: swap; - font-weight: 600; - src: local("Source Code Pro Medium"), local("SourceCodePro-Medium"), url("/fonts/static/SourceCodePro-Medium.woff2") format("woff2"), url("/fonts/static/SourceCodePro-Medium.ttf") format("truetype"); -} - -@font-face { - font-family: 'Source Code Pro'; - font-style: italic; - font-display: swap; - font-weight: 600; - src: local("Source Code Pro Medium Italic"), local("SourceCodePro-MediumItalic"), url("/fonts/static/SourceCodePro-MediumItalic.woff2") format("woff2"), url("/fonts/static/SourceCodePro-MediumItalic.ttf") format("truetype"); -} - -* { - font-family: 'Source Sans 3', sans-serif; -} - -code { - font-family: 'Source Code Pro', monospace; -} - -/* _layout.sass */ -/* Variables */ -html { - background: #0a0c11; -} - -/* Base Layout */ -body { - background: #10131a; - color: #ffffff; - font-family: 'Segoe UI', 'Helvetica Neue', Arial, sans-serif; - width: 100%; - height: 100%; - max-width: 1024px; - margin: 1.5rem auto; - padding: 1.5rem; - box-sizing: border-box; - border-radius: 8px; -} - -header { - background: #1a1e29; - margin: 1.5rem; - padding: 1.5rem; - display: flex; - flex-wrap: wrap; - align-items: center; - justify-content: space-between; - border-radius: 8px; - margin: 0 auto; -} - -header h1, header h1 a { - margin: 0; - font-size: 1.6rem; - font-weight: 900; - color: #ffffff; - text-decoration: none; - padding: 0; - transition: color 0.4s ease-in-out; -} - -header h1:hover, header h1:focus, header h1 a:hover, header h1 a:focus { - color: #6fffd2; -} - -nav { - display: flex; - gap: 1.5rem; - align-items: center; -} - -nav ul { - list-style: none; - margin: 0; - padding: 0; - display: flex; - gap: 0.5rem; - flex-wrap: wrap; -} - -nav ul li { - margin: 0; - padding: 0; -} - -nav ul li a { - padding: 0.4rem 0.6rem; - border-radius: 8px; - background: #1a3e70; - color: #ffffff; - text-decoration: none; - font-weight: 500; - transition: background 0.4s ease-in-out; -} - -nav ul li a:hover, nav ul li a:focus { - background: #00897b; - color: #ffffff; -} - -@media (max-width: 600px) { - header { - flex-direction: column; - align-items: flex-start; - gap: 1.5rem; - } - nav { - width: 100%; - justify-content: flex-start; - margin-top: 1.5rem; - } -} - -main { - margin: 1.5rem 0; - padding: 1.5rem; -} - -footer { - background: #1a1e29; - margin: 1.5rem; - padding: 1.5rem; - border-radius: 8px; - margin: 0 auto; - text-align: center; -} - -footer p { - margin: 0; - font-size: 0.9rem; - color: #bfc9e6; - text-align: center; -} - -section { - border-bottom: 3px solid #1a1e29; - margin: 2rem 0; - padding-bottom: 2rem; -} - -#page-header { - border-bottom: 3px solid #1a1e29; - margin: 2rem 0; - padding-bottom: 2rem; - text-align: center; -} - -#page-header h1 { - margin: 0; - width: 100%; - font-size: 3rem; - word-break: break-word; -} - -#page-header .subtitle { - margin: 0; - width: 100%; - font-size: 1.2rem; - font-weight: 300; - color: #bfc9e6; -} - -.time { - font-size: 0.8rem; - color: #bfc9e6; - text-align: center; -} - -article { - background: #1a1e29; - border-radius: 8px; - padding: 1.5rem; - margin: 1.5rem 0; - position: relative; - transition: background 0.5s ease-in-out; -} - -article:hover, article:focus { - background: #1a3e70; -} - -article h3 { - margin: 0; - font-size: 1.5rem; - font-weight: 700; - color: #ffffff; -} - -article a { - color: #ffffff; - position: absolute; - top: 0; - left: 0; - width: 100%; - height: 100%; - z-index: 1; - text-indent: -9999px; - overflow: hidden; - text-decoration: none; - transition: color 0.3s ease-in-out; -} - -article a:hover, article a:focus { - color: #6fffd2; -} - -article:not(a) { - position: relative; - z-index: 2; -} - -article p { - margin: 0.5rem 0; - font-size: 1rem; - color: #bfc9e6; - font-weight: 300; -} - -article .subtitle { - margin: 0 0 0 0.5rem; - width: 100%; - font-size: 1.1rem; - font-weight: 300; - color: #bfc9e6; -} - -.term-title { - font-weight: 700; - padding: 0.3rem 0.8rem; - margin-bottom: 0.5rem; - border-radius: 8px; -} - -p code { - background: #102747; - margin: 0 0.2rem; - padding: 0.2rem 0.4rem; - border-radius: 5px; - font-size: 0.8rem; -} - -pre { - padding: 0.5rem; - border-radius: 5px; - overflow-x: auto; -} - -pre code { - font-size: 0.8rem; -} - -table#taxonomy-table { - width: 100%; - border-collapse: collapse; - box-sizing: border-box; - background: #1a1e29; - text-align: left; -} - -table#taxonomy-table tr { - border-bottom: 3px solid #10131a; -} - -table#taxonomy-table tr:nth-child(even) { - background: #161923; - transition: background 0.4s ease-in-out; -} - -table#taxonomy-table tr:nth-child(odd) { - background: #202532; - transition: background 0.4s ease-in-out; -} - -table#taxonomy-table tr:hover, table#taxonomy-table tr:focus { - background: #3a4054; -} - -table#taxonomy-table thead { - text-align: left; - border: none; - border-radius: 8px 8px 0 0; -} - -table#taxonomy-table th { - color: #ffffff; - background: #0a0c11 !important; - padding: 0.6rem 0.6rem; - text-align: left; - font-weight: 600; - border: none; -} - -table#taxonomy-table td { - padding: 0.3rem 0.6rem; - text-align: left; - font-weight: 600; - border: none; -} - -table#taxonomy-table td.description { - font-weight: 300; - color: #bfc9e6; -} - -table#taxonomy-table td.tool { - min-width: 100px; -} - -table#taxonomy-table a.term-link { - padding: 0.2rem 0.6rem; - margin: 0.2rem; - display: inline-block; - border-radius: 8px; - text-decoration: none; - font-weight: 500; - color: #ffffff; - transition: color 0.4s ease-in-out, background 0.4s ease-in-out; -} - -table#taxonomy-table a.term-link:hover, table#taxonomy-table a.term-link:focus { - color: #0a0c11 !important; - background: #bfc9e6 !important; -} - -table#taxonomy-table a.taxonomy-name { - padding: 0; - margin: 0.2rem; - display: inline-block; - border-radius: 8px; - text-decoration: none; - font-weight: 500; - color: #ffffff; - transition: color 0.4s ease-in-out; -} - -table#taxonomy-table a.taxonomy-name:hover, table#taxonomy-table a.taxonomy-name:focus { - color: #6fffd2; -} - -table#taxonomy-table a { - color: #ffffff; - text-decoration: none; -} - -table#taxonomy-table a:hover, table#taxonomy-table a:focus { - color: #1de9b6; -} - -#taxonomy-page a.term-link { - padding: 0.3rem 1.2rem; - margin: 0.2rem; - display: inline-block; - border-radius: 8px; - text-decoration: none; - font-weight: 500; - font-size: 1.2rem; - color: #ffffff; - transition: color 0.4s ease-in-out, background 0.4s ease-in-out; -} - -#taxonomy-page a.term-link:hover, #taxonomy-page a.term-link:focus { - color: #0a0c11 !important; - background: #bfc9e6 !important; -} - -/* _text.sass */ -a { - color: #6fffd2; - text-decoration: underline; - transition: color 0.3s ease-in-out; -} - -a:hover, a:focus { - color: #3380ff; -} - -#quick-links { - text-align: left; -} - -#link-list { - display: flex; - gap: 1.5rem; - align-items: center; - flex-wrap: wrap; - margin: 2rem 0 1.5rem 0; - justify-content: center; -} - -#link-list h2 { - flex: none; -} - -#link-list ul { - list-style: none; - margin: 0; - padding: 0; - display: flex; - gap: 1rem; - flex-wrap: wrap; -} - -#link-list ul li { - margin: 0; - padding: 0; -} - -#link-list ul li a { - padding: 0.3rem 0.6rem; - border-radius: 8px; - background: #8fc6ff; - color: #0a0c11; - text-decoration: none; - font-weight: 500; - transition: background 0.3s ease-in-out; -} - -#link-list ul li a:hover, #link-list ul li a:focus { - background: #6fffd2; -} - -a.button { - padding: 0.3rem 0.6rem; - margin: 0 0.2rem; - border-radius: 8px; - background: #8fc6ff; - color: #0a0c11; - text-decoration: none; - font-weight: 500; - transition: background 0.3s ease-in-out; -} - -a.button:hover, a.button:focus { - background: #6fffd2; -} - -#publications { - font-weight: 300; -} - -#publications ul { - list-style: none; - margin: 0; - padding: 0; - display: flex; - flex-direction: column; - gap: 1em; -} - -#publications ul li { - background: #1a1e29; - border-radius: 8px; - padding: 1em 1.5em; -} - -#publications a { - color: #8fc6ff; - text-decoration: none; - font-weight: 100; - transition: color 0.3s ease-in-out; -} - -#publications a:hover, #publications a:focus { - color: #6fffd2; -} - -/*# sourceMappingURL=styles.css.map */ \ No newline at end of file diff --git a/developers/albert-ludwigs-universität/index.html b/developers/albert-ludwigs-universität/index.html index 1d8a877..5adca3f 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 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - ParaFROST + + ParaFROST ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … diff --git a/developers/albert-ludwigs-universität/index.xml b/developers/albert-ludwigs-universität/index.xml index 72b2c24..fa99271 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 - http://localhost:1313/developers/albert-ludwigs-universit%C3%A4t/ + https://example.org/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 - http://localhost:1313/tools/z3-copy/ + https://example.org/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3-copy/ + https://example.org/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/licenses/gpl3/index.html b/developers/cea/index.html similarity index 55% rename from licenses/gpl3/index.html rename to developers/cea/index.html index a01414b..9a91dd7 100644 --- a/licenses/gpl3/index.html +++ b/developers/cea/index.html @@ -1,29 +1,29 @@ - + -GPL3 | Formal Methods Tools +CEA | Formal Methods Tools - + - + - + - - - - + + + + - + @@ -64,8 +64,8 @@ - GPL3 + style="background:rgba(69,53,67,0.4)"> + CEA @@ -81,6 +81,15 @@ + + Colibri + Colibri is an SMT solver. + + + + + + diff --git a/developers/cea/index.xml b/developers/cea/index.xml new file mode 100644 index 0000000..06e663b --- /dev/null +++ b/developers/cea/index.xml @@ -0,0 +1,19 @@ + + + + CEA on Formal Methods Tools + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 796b30d..65532f4 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 @@ - + - + - - - - + + + + - + @@ -81,9 +81,9 @@ - - MathSAT - [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … + + MathSAT + [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … diff --git a/developers/disi-university-of-trento/index.xml b/developers/disi-university-of-trento/index.xml index c03218f..05790f9 100644 --- a/developers/disi-university-of-trento/index.xml +++ b/developers/disi-university-of-trento/index.xml @@ -2,18 +2,18 @@ DISI-University of Trento on Formal Methods Tools - http://localhost:1313/developers/disi-university-of-trento/ + https://example.org/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 - http://localhost:1313/tools/mathsat/ + https://example.org/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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(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> + https://example.org/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 64b6749..f29d58e 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 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - ParaFROST + + ParaFROST ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … diff --git a/developers/eindhoven-university-of-technology/index.xml b/developers/eindhoven-university-of-technology/index.xml index f32cff0..9233983 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 - http://localhost:1313/developers/eindhoven-university-of-technology/ + https://example.org/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 - http://localhost:1313/tools/z3-copy/ + https://example.org/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3-copy/ + https://example.org/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 95fcda9..1786b86 100644 --- a/developers/fondazione-bruno-kessler/index.html +++ b/developers/fondazione-bruno-kessler/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,9 +81,9 @@ - - MathSAT - [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … + + MathSAT + [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … diff --git a/developers/fondazione-bruno-kessler/index.xml b/developers/fondazione-bruno-kessler/index.xml index 380a77a..c7231af 100644 --- a/developers/fondazione-bruno-kessler/index.xml +++ b/developers/fondazione-bruno-kessler/index.xml @@ -2,18 +2,18 @@ Fondazione Bruno Kessler on Formal Methods Tools - http://localhost:1313/developers/fondazione-bruno-kessler/ + https://example.org/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 - http://localhost:1313/tools/mathsat/ + https://example.org/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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(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> + https://example.org/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 8db7642..b909680 100644 --- a/developers/gilles-audemard/index.html +++ b/developers/gilles-audemard/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Glucose + + Glucose Glucose is a SAT solver. diff --git a/developers/gilles-audemard/index.xml b/developers/gilles-audemard/index.xml index ade75d9..3c9b927 100644 --- a/developers/gilles-audemard/index.xml +++ b/developers/gilles-audemard/index.xml @@ -2,17 +2,17 @@ Gilles Audemard on Formal Methods Tools - http://localhost:1313/developers/gilles-audemard/ + https://example.org/developers/gilles-audemard/ Recent content in Gilles Audemard on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Glucose - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/developers/index.html b/developers/index.html index ec33a28..bad591d 100644 --- a/developers/index.html +++ b/developers/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -70,6 +70,168 @@ + + Albert-Ludwigs-Universität + + + + + + + + + + + + + + CEA + + + + + + + + + + + + + + DISI-University of Trento + + + + + + + + + + + + + + Eindhoven University of Technology + + + + + + + + + + + + + + Fondazione Bruno Kessler + + + + + + + + + + + + + + Gilles Audemard + + + + + + + + + + + + + + INRIA Rhône-Alpes + + + + + + + + + + + + + + Johannes Kepler Universität Linz + + + + + + + + + + + + + + Laurent Simon + + + + + + + + + + + + + Masaryk University + + + + + + + + + + + + + Niklas Eén + + + + + + + + + + + + + + Niklas Sörensson + + + + + + + + + + + + + + Norbert Manthey + + + + + + + + + + + + + + + + + + + + + + + University of Iowa + + + + + + + + + + + + + + University of Lugano + + + + + + + + + + + + + + University of Virginia + + + diff --git a/developers/index.xml b/developers/index.xml index 1cc2a9a..6ff8e08 100644 --- a/developers/index.xml +++ b/developers/index.xml @@ -2,66 +2,178 @@ Developers on Formal Methods Tools - http://localhost:1313/developers/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/albert-ludwigs-universit%C3%A4t/ + + + + CEA + https://example.org/developers/cea/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/cea/ + + + + DISI-University of Trento + https://example.org/developers/disi-university-of-trento/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/disi-university-of-trento/ + + + + Eindhoven University of Technology + https://example.org/developers/eindhoven-university-of-technology/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/eindhoven-university-of-technology/ + + + + Fondazione Bruno Kessler + https://example.org/developers/fondazione-bruno-kessler/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/fondazione-bruno-kessler/ + + + + Gilles Audemard + https://example.org/developers/gilles-audemard/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/gilles-audemard/ + + + + INRIA Rhône-Alpes + https://example.org/developers/inria-rh%C3%B4ne-alpes/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/inria-rh%C3%B4ne-alpes/ + + + + Johannes Kepler Universität Linz + https://example.org/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/ + + + + Laurent Simon + https://example.org/developers/laurent-simon/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/laurent-simon/ + + LORIA - http://localhost:1313/developers/loria/ + https://example.org/developers/loria/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/loria/ + https://example.org/developers/loria/ + + + + Masaryk University + https://example.org/developers/masaryk-university/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/masaryk-university/ Microsoft Research - http://localhost:1313/developers/microsoft-research/ + https://example.org/developers/microsoft-research/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/microsoft-research/ + https://example.org/developers/microsoft-research/ + + + + Niklas Eén + https://example.org/developers/niklas-e%C3%A9n/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/niklas-e%C3%A9n/ + + + + Niklas Sörensson + https://example.org/developers/niklas-s%C3%B6rensson/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/niklas-s%C3%B6rensson/ + + + + Norbert Manthey + https://example.org/developers/norbert-manthey/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/norbert-manthey/ RWTH Aachen - http://localhost:1313/developers/rwth-aachen/ + https://example.org/developers/rwth-aachen/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/rwth-aachen/ + https://example.org/developers/rwth-aachen/ SRI International - http://localhost:1313/developers/sri-international/ + https://example.org/developers/sri-international/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/sri-international/ + https://example.org/developers/sri-international/ Stanford University - http://localhost:1313/developers/stanford-university/ + https://example.org/developers/stanford-university/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/stanford-university/ + https://example.org/developers/stanford-university/ ULiege - http://localhost:1313/developers/uliege/ + https://example.org/developers/uliege/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/uliege/ + https://example.org/developers/uliege/ University of Freiburg - http://localhost:1313/developers/university-of-freiburg/ + https://example.org/developers/university-of-freiburg/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/university-of-freiburg/ + https://example.org/developers/university-of-freiburg/ University of Illinois - http://localhost:1313/developers/university-of-illinois/ + https://example.org/developers/university-of-illinois/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/developers/university-of-illinois/ + https://example.org/developers/university-of-illinois/ + + + + University of Iowa + https://example.org/developers/university-of-iowa/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/university-of-iowa/ + + + + University of Lugano + https://example.org/developers/university-of-lugano/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/university-of-lugano/ + + + + University of Virginia + https://example.org/developers/university-of-virginia/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/developers/university-of-virginia/ diff --git a/maintenance/archived/index.html b/developers/inria-rhône-alpes/index.html similarity index 54% rename from maintenance/archived/index.html rename to developers/inria-rhône-alpes/index.html index b3a5c14..73d8984 100644 --- a/maintenance/archived/index.html +++ b/developers/inria-rhône-alpes/index.html @@ -1,29 +1,29 @@ - + -Archived | Formal Methods Tools +INRIA Rhône-Alpes | Formal Methods Tools - + - + - + - - - - + + + + - + @@ -64,8 +64,8 @@ - Archived + style="background:rgba(20,228,136,0.4)"> + INRIA Rhône-Alpes @@ -81,10 +81,10 @@ - - Riss - Riss is a SAT solving tool collection that was updated until 2017. - + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … diff --git a/developers/inria-rhône-alpes/index.xml b/developers/inria-rhône-alpes/index.xml new file mode 100644 index 0000000..d1c745d --- /dev/null +++ b/developers/inria-rhône-alpes/index.xml @@ -0,0 +1,19 @@ + + + + INRIA Rhône-Alpes on Formal Methods Tools + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 c1b4baf..00ef7dd 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 @@ - + - + - - - - + + + + - + @@ -81,9 +81,18 @@ - - MathSAT - [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + Lingeling + Lingeling is a SAT solver. + diff --git a/developers/johannes-kepler-universität-linz/index.xml b/developers/johannes-kepler-universität-linz/index.xml index 5416b5b..f19a512 100644 --- a/developers/johannes-kepler-universität-linz/index.xml +++ b/developers/johannes-kepler-universität-linz/index.xml @@ -2,18 +2,25 @@ Johannes Kepler Universität Linz on Formal Methods Tools - http://localhost:1313/developers/johannes-kepler-universit%C3%A4t-linz/ + https://example.org/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 - + - MathSAT - http://localhost:1313/tools/mathsat/ + Boolector + https://example.org/tools/sat-smt/boolector/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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> + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 3a4b58e..9c11f3f 100644 --- a/developers/laurent-simon/index.html +++ b/developers/laurent-simon/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Glucose + + Glucose Glucose is a SAT solver. diff --git a/developers/laurent-simon/index.xml b/developers/laurent-simon/index.xml index b5ca25d..f9314b9 100644 --- a/developers/laurent-simon/index.xml +++ b/developers/laurent-simon/index.xml @@ -2,17 +2,17 @@ Laurent Simon on Formal Methods Tools - http://localhost:1313/developers/laurent-simon/ + https://example.org/developers/laurent-simon/ Recent content in Laurent Simon on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Glucose - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/developers/loria/index.html b/developers/loria/index.html index 89ae1e1..fed4cbf 100644 --- a/developers/loria/index.html +++ b/developers/loria/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - veriT + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … diff --git a/developers/loria/index.xml b/developers/loria/index.xml index db30ec1..8aa6973 100644 --- a/developers/loria/index.xml +++ b/developers/loria/index.xml @@ -2,17 +2,17 @@ LORIA on Formal Methods Tools - http://localhost:1313/developers/loria/ + https://example.org/developers/loria/ Recent content in LORIA on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + veriT - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 6f6d65a..beb5063 100644 --- a/developers/masaryk-university/index.html +++ b/developers/masaryk-university/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Q3B + + Q3B [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … diff --git a/developers/masaryk-university/index.xml b/developers/masaryk-university/index.xml index 35706b2..2f36b3b 100644 --- a/developers/masaryk-university/index.xml +++ b/developers/masaryk-university/index.xml @@ -2,17 +2,17 @@ Masaryk University on Formal Methods Tools - http://localhost:1313/developers/masaryk-university/ + https://example.org/developers/masaryk-university/ Recent content in Masaryk University on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Q3B - http://localhost:1313/tools/q3b/ + https://example.org/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/q3b/ + https://example.org/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 c51079c..29cd673 100644 --- a/developers/microsoft-research/index.html +++ b/developers/microsoft-research/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/developers/microsoft-research/index.xml b/developers/microsoft-research/index.xml index b4e9b8b..7e073ce 100644 --- a/developers/microsoft-research/index.xml +++ b/developers/microsoft-research/index.xml @@ -2,17 +2,17 @@ Microsoft Research on Formal Methods Tools - http://localhost:1313/developers/microsoft-research/ + https://example.org/developers/microsoft-research/ Recent content in Microsoft Research on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Z3 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 e07af04..5eb134f 100644 --- a/developers/niklas-eén/index.html +++ b/developers/niklas-eén/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,9 +81,9 @@ - - MiniSat - MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers … + + MiniSat + [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … diff --git a/developers/niklas-eén/index.xml b/developers/niklas-eén/index.xml index 233b6a1..8cfe3df 100644 --- a/developers/niklas-eén/index.xml +++ b/developers/niklas-eén/index.xml @@ -2,18 +2,18 @@ Niklas Eén on Formal Methods Tools - http://localhost:1313/developers/niklas-e%C3%A9n/ + https://example.org/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 - http://localhost:1313/tools/minisat/ + https://example.org/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/minisat/ - <p>MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + https://example.org/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 69c2d13..2363d81 100644 --- a/developers/niklas-sörensson/index.html +++ b/developers/niklas-sörensson/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,9 +81,9 @@ - - MiniSat - MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers … + + MiniSat + [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … diff --git a/developers/niklas-sörensson/index.xml b/developers/niklas-sörensson/index.xml index 9d0236b..e387246 100644 --- a/developers/niklas-sörensson/index.xml +++ b/developers/niklas-sörensson/index.xml @@ -2,18 +2,18 @@ Niklas Sörensson on Formal Methods Tools - http://localhost:1313/developers/niklas-s%C3%B6rensson/ + https://example.org/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 - http://localhost:1313/tools/minisat/ + https://example.org/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/minisat/ - <p>MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.</p> + https://example.org/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 5002c3b..f4e1c3a 100644 --- a/developers/norbert-manthey/index.html +++ b/developers/norbert-manthey/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Riss + + Riss [ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. diff --git a/developers/norbert-manthey/index.xml b/developers/norbert-manthey/index.xml index 9c8d757..ab73409 100644 --- a/developers/norbert-manthey/index.xml +++ b/developers/norbert-manthey/index.xml @@ -2,17 +2,17 @@ Norbert Manthey on Formal Methods Tools - http://localhost:1313/developers/norbert-manthey/ + https://example.org/developers/norbert-manthey/ Recent content in Norbert Manthey on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Riss - http://localhost:1313/tools/riss/ + https://example.org/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/riss/ + https://example.org/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 0e72f51..4cf24fb 100644 --- a/developers/rwth-aachen/index.html +++ b/developers/rwth-aachen/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - SMT-RAT + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … diff --git a/developers/rwth-aachen/index.xml b/developers/rwth-aachen/index.xml index dfcadf0..01fb0ed 100644 --- a/developers/rwth-aachen/index.xml +++ b/developers/rwth-aachen/index.xml @@ -2,17 +2,17 @@ RWTH Aachen on Formal Methods Tools - http://localhost:1313/developers/rwth-aachen/ + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 df4ad49..e50ed81 100644 --- a/developers/sri-international/index.html +++ b/developers/sri-international/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … diff --git a/developers/sri-international/index.xml b/developers/sri-international/index.xml index 9d32cec..ed3c296 100644 --- a/developers/sri-international/index.xml +++ b/developers/sri-international/index.xml @@ -2,17 +2,17 @@ SRI International on Formal Methods Tools - http://localhost:1313/developers/sri-international/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 7cdb8b2..8aa08d9 100644 --- a/developers/stanford-university/index.html +++ b/developers/stanford-university/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,41 @@ - - STP + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … + + + + + + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … diff --git a/developers/stanford-university/index.xml b/developers/stanford-university/index.xml index b9e5149..6b7553b 100644 --- a/developers/stanford-university/index.xml +++ b/developers/stanford-university/index.xml @@ -2,17 +2,45 @@ Stanford University on Formal Methods Tools - http://localhost:1313/developers/stanford-university/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + STP - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 822aa83..02a3212 100644 --- a/developers/uliege/index.html +++ b/developers/uliege/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - veriT + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … diff --git a/developers/uliege/index.xml b/developers/uliege/index.xml index 9660980..cd3ac19 100644 --- a/developers/uliege/index.xml +++ b/developers/uliege/index.xml @@ -2,17 +2,17 @@ ULiege on Formal Methods Tools - http://localhost:1313/developers/uliege/ + https://example.org/developers/uliege/ Recent content in ULiege on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + veriT - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 9d92152..955966d 100644 --- a/developers/university-of-freiburg/index.html +++ b/developers/university-of-freiburg/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,16 +81,8 @@ - - Riss - Not Maintained Since {map[year:2017] /home/landon/gitea/fmtools/content/tools/riss.md <nil> … - - - - - - - SMTInterpol + + SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and … diff --git a/developers/university-of-freiburg/index.xml b/developers/university-of-freiburg/index.xml index 309612c..2880da0 100644 --- a/developers/university-of-freiburg/index.xml +++ b/developers/university-of-freiburg/index.xml @@ -2,24 +2,17 @@ University of Freiburg on Formal Methods Tools - http://localhost:1313/developers/university-of-freiburg/ + https://example.org/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 - - - Riss - http://localhost:1313/tools/riss/ - Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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(226, 59, 59);"></span> <span style="color: rgb(226, 59, 59); font-size: 1rem;">Not Maintained Since {map[year:2017] /home/landon/gitea/fmtools/content/tools/riss.md &lt;nil&gt; inactive true 0 {{} {{} 0} {{} {0 0}}} {{} {{} 0} {{} {0 0}}} 615 { 0 0 0} &lt;nil&gt;}</span> </div> Riss is a SAT solving tool collection that was updated until 2017.</p> - + SMTInterpol - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 ac2f82c..202ff36 100644 --- a/developers/university-of-illinois/index.html +++ b/developers/university-of-illinois/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … diff --git a/developers/university-of-illinois/index.xml b/developers/university-of-illinois/index.xml index 6e5b0b0..cd7aade 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 - http://localhost:1313/developers/university-of-illinois/ + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 new file mode 100644 index 0000000..463bf33 --- /dev/null +++ b/developers/university-of-iowa/index.html @@ -0,0 +1,112 @@ + + + + + + + + +University of Iowa | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + University of Iowa + +

+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + +
ToolDescription
cvc4 [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded …
cvc5cvc5 is an automatic theorem prover for SMT problems. +
+ +
+ + + diff --git a/developers/university-of-iowa/index.xml b/developers/university-of-iowa/index.xml new file mode 100644 index 0000000..04ad907 --- /dev/null +++ b/developers/university-of-iowa/index.xml @@ -0,0 +1,26 @@ + + + + University of Iowa on Formal Methods Tools + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 c64615e..923fff8 100644 --- a/developers/university-of-lugano/index.html +++ b/developers/university-of-lugano/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - OpenSMT + + OpenSMT OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … diff --git a/developers/university-of-lugano/index.xml b/developers/university-of-lugano/index.xml index 4a5b7a9..62c4f66 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 - http://localhost:1313/developers/university-of-lugano/ + https://example.org/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 - http://localhost:1313/tools/opensmt/ + https://example.org/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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> + 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> diff --git a/maintenance/not-active/index.html b/developers/university-of-virginia/index.html similarity index 54% rename from maintenance/not-active/index.html rename to developers/university-of-virginia/index.html index 9c13306..7025330 100644 --- a/maintenance/not-active/index.html +++ b/developers/university-of-virginia/index.html @@ -1,29 +1,29 @@ - + -Not Active | Formal Methods Tools +University of Virginia | Formal Methods Tools - + - + - + - - - - + + + + - + @@ -64,8 +64,8 @@ - Not Active + style="background:rgba(207,199,132,0.4)"> + University of Virginia @@ -81,10 +81,10 @@ - - Riss - Riss is a SAT solving tool collection that was updated until 2017. - + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … diff --git a/developers/university-of-virginia/index.xml b/developers/university-of-virginia/index.xml new file mode 100644 index 0000000..b5ff199 --- /dev/null +++ b/developers/university-of-virginia/index.xml @@ -0,0 +1,19 @@ + + + + University of Virginia on Formal Methods Tools + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 aaaa8b1..36c762b 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 b61f720..b960c67 100644 --- a/domains/index.xml +++ b/domains/index.xml @@ -2,10 +2,10 @@ Domains on Formal Methods Tools - http://localhost:1313/domains/ + https://example.org/domains/ Recent content in Domains on Formal Methods Tools Hugo en-us - + diff --git a/index.html b/index.html index 7bfa8ee..85a6002 100644 --- a/index.html +++ b/index.html @@ -1,7 +1,7 @@ - + @@ -15,16 +15,16 @@ - + - + - - - - + + + + - + @@ -90,122 +90,8 @@ Contribute
-

Featured Tools

- -
-

- SMTInterpol - - Interpolating SMT Solver - -

-

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

- SMTInterpol -
- -
-

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

- OpenSMT - - SMT Solver - -

-

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

- OpenSMT -
- -
-

- ParaFROST - - SMT Solver - -

-

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

- ParaFROST -
- -
-

- MiniSat - - SAT Solver - -

-

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

- MiniSat -
- -
-

- Riss - - SAT Tool Collection - -

-

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

- Riss -
- -
-

- Z3 - - Theorem Prover - -

-

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

- Z3 -
- -
-

- Q3B - - SMT Solver - -

-

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

- Q3B -
- -
-

- Lingeling - - SMT Solver - -

-

Lingeling is a SAT solver. -

- Lingeling -
- -
-

- veriT - - SMT Solver - -

-

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

- veriT -
+

Try Something New

+

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

@@ -217,7 +103,19 @@ APIs and Bindings This tool is available …

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

- SMT-RAT + SMT-RAT +

+ +
+

+ cvc5 + + Theorem Prover + +

+

cvc5 is an automatic theorem prover for SMT problems. +

+ cvc5
@@ -228,19 +126,75 @@ C++ API: …

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

- MathSAT + MathSAT

- STP + dReal - Simple Theorem Prover + SMT Solver

-

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

- STP +

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

+ dReal +
+ +
+

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

+ cvc4 + + Theorem Prover + +

+

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

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

+

Lingeling is a SAT solver. +

+ Lingeling
@@ -252,7 +206,124 @@ APIs and Bindings This tool is available through the following …

Glucose is a SAT solver.

- Glucose + Glucose +
+ +
+

+ Riss + + SAT Tool Collection + +

+

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

+ Riss +
+ +
+

+ Boolector + + SMT Solver + +

+

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

+ Boolector +
+ +
+

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

+

CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following interfaces: +C++ Namespace: …

+ CryptoMiniSat +
+ +
+

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

+

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

+ OpenSMT +
+ +
+

+ Z3 + + Theorem Prover + +

+

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

+ Z3 +
+ +
+

+ 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
diff --git a/index.xml b/index.xml index ccf093e..0191d72 100644 --- a/index.xml +++ b/index.xml @@ -2,137 +2,186 @@ The Ultimate Formal Methods Toolbox on Formal Methods Tools - http://localhost:1313/ + https://example.org/ 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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/colibri/ + <p>Colibri is an SMT solver.</p> + + + CryptoMiniSat + https://example.org/tools/sat-smt/cryptominisat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + + dReal + https://example.org/tools/sat-smt/dreal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> Lingeling - http://localhost:1313/tools/lingeling/ + https://example.org/tools/sat-smt/lingeling/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/lingeling/ + https://example.org/tools/sat-smt/lingeling/ <p>Lingeling is a SAT solver.</p> MathSAT - http://localhost:1313/tools/mathsat/ + https://example.org/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/mathsat/ + https://example.org/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 - http://localhost:1313/tools/minisat/ + https://example.org/tools/sat-smt/minisat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/minisat/ + https://example.org/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 - http://localhost:1313/tools/opensmt/ + https://example.org/tools/sat-smt/opensmt/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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> + 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> ParaFROST - http://localhost:1313/tools/parafrost/ + https://example.org/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/parafrost/ + https://example.org/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 - http://localhost:1313/tools/q3b/ + https://example.org/tools/sat-smt/q3b/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/q3b/ + https://example.org/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 - http://localhost:1313/tools/riss/ + https://example.org/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/riss/ + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 - http://localhost:1313/about/ + https://example.org/about/ Mon, 01 Jan 0001 00:00:00 +0000 - http://localhost:1313/about/ + https://example.org/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 - http://localhost:1313/contribute/ + https://example.org/contribute/ Mon, 01 Jan 0001 00:00:00 +0000 - http://localhost:1313/contribute/ + 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> MIT License - http://localhost:1313/license/ + https://example.org/license/ Mon, 01 Jan 0001 00:00:00 +0000 - http://localhost:1313/license/ + https://example.org/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 - http://localhost:1313/privacy/ + https://example.org/privacy/ Mon, 01 Jan 0001 00:00:00 +0000 - 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</p> <p>If you choose to contribute content (such as submitting an article or comment), any information you voluntarily provide will be stored as part of the website&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. Any information you voluntarily provide as part of a code contribution becomes public information and may be used by the general public as allowed by respective laws and policies.</p> + https://example.org/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 24e6049..3e25693 100644 --- a/inputs/cnf/index.html +++ b/inputs/cnf/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,17 @@ - - Glucose + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … + + + + + + + Glucose Glucose is a SAT solver. diff --git a/inputs/cnf/index.xml b/inputs/cnf/index.xml index fc87635..7bde3b5 100644 --- a/inputs/cnf/index.xml +++ b/inputs/cnf/index.xml @@ -2,17 +2,24 @@ CNF on Formal Methods Tools - http://localhost:1313/inputs/cnf/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/glucose/ + https://example.org/tools/sat-smt/glucose/ <p>Glucose is a SAT solver.</p> diff --git a/inputs/dimacs/index.html b/inputs/dimacs/index.html index 7b367ef..6f6372a 100644 --- a/inputs/dimacs/index.html +++ b/inputs/dimacs/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,16 +81,16 @@ - - veriT + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/inputs/dimacs/index.xml b/inputs/dimacs/index.xml index 8fc7f84..d72aacd 100644 --- a/inputs/dimacs/index.xml +++ b/inputs/dimacs/index.xml @@ -2,24 +2,24 @@ DIMACS on Formal Methods Tools - http://localhost:1313/inputs/dimacs/ + https://example.org/inputs/dimacs/ Recent content in DIMACS on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + veriT - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 1e30ce3..b24e977 100644 --- a/inputs/index.html +++ b/inputs/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -70,6 +70,24 @@ + + CNF + + + + + + + + + + + + Inputs on Formal Methods Tools - http://localhost:1313/inputs/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/inputs/cnf/ + + DIMACS - http://localhost:1313/inputs/dimacs/ + https://example.org/inputs/dimacs/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/inputs/dimacs/ + https://example.org/inputs/dimacs/ SMTLIB2 - http://localhost:1313/inputs/smtlib2/ + https://example.org/inputs/smtlib2/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/inputs/smtlib2/ + https://example.org/inputs/smtlib2/ Yices 2 - http://localhost:1313/inputs/yices-2/ + https://example.org/inputs/yices-2/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/inputs/yices-2/ + https://example.org/inputs/yices-2/ diff --git a/inputs/smtlib2/index.html b/inputs/smtlib2/index.html index 7761ccc..878be45 100644 --- a/inputs/smtlib2/index.html +++ b/inputs/smtlib2/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,74 @@ - - SMT-RAT + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … + + + + + + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + Colibri + Colibri is an SMT solver. + + + + + + + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + OpenSMT + OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … + + + + + + + ParaFROST + ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … + + + + + + + Q3B + [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … + + + + + + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … @@ -90,8 +156,8 @@ APIs and Bindings This tool is available through the … - - SMTInterpol + + SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and … @@ -99,8 +165,8 @@ APIs and … - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -108,24 +174,24 @@ APIs and Bindings This tool is available … - - veriT + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/inputs/smtlib2/index.xml b/inputs/smtlib2/index.xml index 3e19112..e864f40 100644 --- a/inputs/smtlib2/index.xml +++ b/inputs/smtlib2/index.xml @@ -2,52 +2,108 @@ SMTLIB2 on Formal Methods Tools - http://localhost:1313/inputs/smtlib2/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/colibri/ + <p>Colibri is an SMT solver.</p> + + + cvc4 + https://example.org/tools/sat-smt/cvc4/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + + OpenSMT + https://example.org/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> + + + ParaFROST + https://example.org/tools/sat-smt/parafrost/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 1f45235..e2a78cc 100644 --- a/inputs/yices-2/index.html +++ b/inputs/yices-2/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … diff --git a/inputs/yices-2/index.xml b/inputs/yices-2/index.xml index 86c15a3..cae8333 100644 --- a/inputs/yices-2/index.xml +++ b/inputs/yices-2/index.xml @@ -2,17 +2,17 @@ Yices 2 on Formal Methods Tools - http://localhost:1313/inputs/yices-2/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 ec56323..95f7211 100644 --- a/interfaces/.net/index.html +++ b/interfaces/.net/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/.net/index.xml b/interfaces/.net/index.xml index 040e11d..46605d7 100644 --- a/interfaces/.net/index.xml +++ b/interfaces/.net/index.xml @@ -2,17 +2,17 @@ .NET on Formal Methods Tools - http://localhost:1313/interfaces/.net/ + https://example.org/interfaces/.net/ Recent content in .NET on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Z3 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 b7126e4..93eaee6 100644 --- a/interfaces/c++/index.html +++ b/interfaces/c++/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,17 @@ - - SMT-RAT + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … + + + + + + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … @@ -90,8 +99,8 @@ APIs and Bindings This tool is available through the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/c++/index.xml b/interfaces/c++/index.xml index 03c18b2..ffe6a18 100644 --- a/interfaces/c++/index.xml +++ b/interfaces/c++/index.xml @@ -2,24 +2,31 @@ C++ on Formal Methods Tools - http://localhost:1313/interfaces/c++/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 0dc0b4c..a155bf7 100644 --- a/interfaces/c/index.html +++ b/interfaces/c/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -90,8 +90,8 @@ APIs and Bindings This tool is available … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/c/index.xml b/interfaces/c/index.xml index 4f72437..6e505e4 100644 --- a/interfaces/c/index.xml +++ b/interfaces/c/index.xml @@ -2,24 +2,24 @@ C on Formal Methods Tools - http://localhost:1313/interfaces/c/ + https://example.org/interfaces/c/ Recent content in C on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + STP - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 c528384..cf83d8b 100644 --- a/interfaces/cli/index.html +++ b/interfaces/cli/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,16 +81,134 @@ - - Riss - Not Maintained Since {map[year:2017] /home/landon/gitea/fmtools/content/tools/riss.md <nil> … + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … - - SMT-RAT + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + Colibri + Colibri is an SMT solver. + + + + + + + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … + + + + + + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + dReal + [ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems … + + + + + + + Glucose + Glucose is a SAT solver. + + + + + + + + Lingeling + Lingeling is a SAT solver. + + + + + + + + MathSAT + [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … + + + + + + + MiniSat + [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … + + + + + + + OpenSMT + OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … + + + + + + + ParaFROST + ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … + + + + + + + Q3B + [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … + + + + + + + Riss + [ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. + + + + + + + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … @@ -98,8 +216,8 @@ APIs and Bindings This tool is available through the … - - SMTInterpol + + SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and … @@ -107,8 +225,8 @@ APIs and … - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -116,24 +234,24 @@ APIs and Bindings This tool is available … - - veriT + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/cli/index.xml b/interfaces/cli/index.xml index 0d13662..c2c2e0e 100644 --- a/interfaces/cli/index.xml +++ b/interfaces/cli/index.xml @@ -2,59 +2,157 @@ CLI on Formal Methods Tools - http://localhost:1313/interfaces/cli/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/colibri/ + <p>Colibri is an SMT solver.</p> + + + CryptoMiniSat + https://example.org/tools/sat-smt/cryptominisat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + + dReal + https://example.org/tools/sat-smt/dreal/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/glucose/ + <p>Glucose is a SAT solver.</p> + + + Lingeling + https://example.org/tools/sat-smt/lingeling/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/lingeling/ + <p>Lingeling is a SAT solver.</p> + + + MathSAT + https://example.org/tools/sat-smt/mathsat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + 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> + + + ParaFROST + https://example.org/tools/sat-smt/parafrost/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/riss/ + https://example.org/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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(226, 59, 59);"></span> <span style="color: rgb(226, 59, 59); font-size: 1rem;">Not Maintained Since {map[year:2017] /home/landon/gitea/fmtools/content/tools/riss.md &lt;nil&gt; inactive true 0 {{} {{} 0} {{} {0 0}}} {{} {{} 0} {{} {0 0}}} 615 { 0 0 0} &lt;nil&gt;}</span> </div> Riss is a SAT solving tool collection that was updated until 2017.</p> + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 abf249a..e880af3 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 43838fd..94d4565 100644 --- a/interfaces/index.xml +++ b/interfaces/index.xml @@ -2,66 +2,66 @@ Interfaces on Formal Methods Tools - http://localhost:1313/interfaces/ + https://example.org/interfaces/ Recent content in Interfaces on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + .NET - http://localhost:1313/interfaces/.net/ + https://example.org/interfaces/.net/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/.net/ + https://example.org/interfaces/.net/ C - http://localhost:1313/interfaces/c/ + https://example.org/interfaces/c/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/c/ + https://example.org/interfaces/c/ C++ - http://localhost:1313/interfaces/c++/ + https://example.org/interfaces/c++/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/c++/ + https://example.org/interfaces/c++/ CLI - http://localhost:1313/interfaces/cli/ + https://example.org/interfaces/cli/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/cli/ + https://example.org/interfaces/cli/ Java - http://localhost:1313/interfaces/java/ + https://example.org/interfaces/java/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/java/ + https://example.org/interfaces/java/ Online - http://localhost:1313/interfaces/online/ + https://example.org/interfaces/online/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/online/ + https://example.org/interfaces/online/ Python - http://localhost:1313/interfaces/python/ + https://example.org/interfaces/python/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/python/ + https://example.org/interfaces/python/ Rust - http://localhost:1313/interfaces/rust/ + https://example.org/interfaces/rust/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/interfaces/rust/ + https://example.org/interfaces/rust/ diff --git a/interfaces/java/index.html b/interfaces/java/index.html index 3b0f8d4..3319a91 100644 --- a/interfaces/java/index.html +++ b/interfaces/java/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - SMTInterpol + + SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and … @@ -90,8 +90,8 @@ APIs and … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/java/index.xml b/interfaces/java/index.xml index 4de8a79..f83e419 100644 --- a/interfaces/java/index.xml +++ b/interfaces/java/index.xml @@ -2,24 +2,24 @@ Java on Formal Methods Tools - http://localhost:1313/interfaces/java/ + https://example.org/interfaces/java/ Recent content in Java on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + SMTInterpol - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 643ce0d..3d19eaa 100644 --- a/interfaces/online/index.html +++ b/interfaces/online/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,25 @@ - - Z3 + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/online/index.xml b/interfaces/online/index.xml index f16678f..b79c910 100644 --- a/interfaces/online/index.xml +++ b/interfaces/online/index.xml @@ -2,17 +2,31 @@ Online on Formal Methods Tools - http://localhost:1313/interfaces/online/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + Z3 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 d941d29..00c35ee 100644 --- a/interfaces/python/index.html +++ b/interfaces/python/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,17 @@ - - STP + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … + + + + + + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -90,16 +99,16 @@ APIs and Bindings This tool is available … - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/python/index.xml b/interfaces/python/index.xml index e4afa05..e8ecb79 100644 --- a/interfaces/python/index.xml +++ b/interfaces/python/index.xml @@ -2,31 +2,38 @@ Python on Formal Methods Tools - http://localhost:1313/interfaces/python/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 8883a97..d200ca4 100644 --- a/interfaces/rust/index.html +++ b/interfaces/rust/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,16 +81,16 @@ - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/interfaces/rust/index.xml b/interfaces/rust/index.xml index bd0284b..213723f 100644 --- a/interfaces/rust/index.xml +++ b/interfaces/rust/index.xml @@ -2,24 +2,24 @@ Rust on Formal Methods Tools - http://localhost:1313/interfaces/rust/ + https://example.org/interfaces/rust/ Recent content in Rust on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Yices 2 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 ad1f6a4..d961d2a 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 73db33f..8833069 100644 --- a/licenses/all-rights-reserved/index.html +++ b/licenses/all-rights-reserved/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,9 +81,9 @@ - - MathSAT - [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … + + MathSAT + [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … diff --git a/licenses/all-rights-reserved/index.xml b/licenses/all-rights-reserved/index.xml index 45879ba..ef314b9 100644 --- a/licenses/all-rights-reserved/index.xml +++ b/licenses/all-rights-reserved/index.xml @@ -2,18 +2,18 @@ All Rights Reserved on Formal Methods Tools - http://localhost:1313/licenses/all-rights-reserved/ + https://example.org/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 - http://localhost:1313/tools/mathsat/ + https://example.org/tools/sat-smt/mathsat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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(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> + https://example.org/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/maintenance/deprecated/index.html b/licenses/apache-2.0/index.html similarity index 54% rename from maintenance/deprecated/index.html rename to licenses/apache-2.0/index.html index 47d5605..09025d6 100644 --- a/maintenance/deprecated/index.html +++ b/licenses/apache-2.0/index.html @@ -1,29 +1,29 @@ - + -Deprecated | Formal Methods Tools +Apache-2.0 | Formal Methods Tools - + - + - + - - - - + + + + - + @@ -64,8 +64,8 @@ - Deprecated + style="background:rgba(242,244,241,0.4)"> + Apache-2.0 @@ -81,10 +81,9 @@ - - Riss - Riss is a SAT solving tool collection that was updated until 2017. - + + dReal + [ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems … diff --git a/licenses/apache-2.0/index.xml b/licenses/apache-2.0/index.xml new file mode 100644 index 0000000..b9ed02c --- /dev/null +++ b/licenses/apache-2.0/index.xml @@ -0,0 +1,19 @@ + + + + Apache-2.0 on Formal Methods Tools + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 61f3fbd..ddb1a22 100644 --- a/licenses/bsd/index.html +++ b/licenses/bsd/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,25 @@ - - veriT + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … diff --git a/licenses/bsd/index.xml b/licenses/bsd/index.xml index c814b17..81b447d 100644 --- a/licenses/bsd/index.xml +++ b/licenses/bsd/index.xml @@ -2,17 +2,31 @@ BSD on Formal Methods Tools - http://localhost:1313/licenses/bsd/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + veriT - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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/gpl3/index.xml b/licenses/gpl3/index.xml deleted file mode 100644 index 2c850a3..0000000 --- a/licenses/gpl3/index.xml +++ /dev/null @@ -1,11 +0,0 @@ - - - - GPL3 on Formal Methods Tools - http://localhost:1313/licenses/gpl3/ - Recent content in GPL3 on Formal Methods Tools - Hugo - en-us - - - diff --git a/licenses/gplv2/index.html b/licenses/gplv2/index.html new file mode 100644 index 0000000..5cf83a7 --- /dev/null +++ b/licenses/gplv2/index.html @@ -0,0 +1,104 @@ + + + + + + + + +GPLv2 | Formal Methods Tools + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+

Formal Methods Tools

+ + + + +
+
+ +

+ + + + + + + GPLv2 + +

+ +
+ + + + + + + + + + + + + + + + + + + + +
ToolDescription
CryptoMiniSatCryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following …
+ +
+ + + diff --git a/licenses/gplv2/index.xml b/licenses/gplv2/index.xml new file mode 100644 index 0000000..84b6a06 --- /dev/null +++ b/licenses/gplv2/index.xml @@ -0,0 +1,19 @@ + + + + GPLv2 on Formal Methods Tools + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 1ad2fe5..153a34b 100644 --- a/licenses/gplv3/index.html +++ b/licenses/gplv3/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,16 +81,24 @@ - - ParaFROST + + OpenSMT + OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … + + + + + + + ParaFROST ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … - - SMTInterpol + + SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and … @@ -98,8 +106,8 @@ APIs and … - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … diff --git a/licenses/gplv3/index.xml b/licenses/gplv3/index.xml index 2d344f5..c79d1b7 100644 --- a/licenses/gplv3/index.xml +++ b/licenses/gplv3/index.xml @@ -2,31 +2,38 @@ GPLv3 on Formal Methods Tools - http://localhost:1313/licenses/gplv3/ + https://example.org/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/ + 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> + ParaFROST - http://localhost:1313/tools/parafrost/ + https://example.org/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/parafrost/ + https://example.org/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 - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 2f4df9f..60b1dec 100644 --- a/licenses/index.html +++ b/licenses/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -70,6 +70,42 @@ + + All Rights Reserved + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + GPLv2 + + + + + + + + + + + + Licenses on Formal Methods Tools - http://localhost:1313/licenses/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/licenses/all-rights-reserved/ + + + + Apache-2.0 + https://example.org/licenses/apache-2.0/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/licenses/apache-2.0/ + + BSD - http://localhost:1313/licenses/bsd/ + https://example.org/licenses/bsd/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/licenses/bsd/ + https://example.org/licenses/bsd/ + + + + GPLv2 + https://example.org/licenses/gplv2/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/licenses/gplv2/ GPLv3 - http://localhost:1313/licenses/gplv3/ + https://example.org/licenses/gplv3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/licenses/gplv3/ + https://example.org/licenses/gplv3/ LGPLv2 - http://localhost:1313/licenses/lgplv2/ + https://example.org/licenses/lgplv2/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/licenses/lgplv2/ + https://example.org/licenses/lgplv2/ MIT - http://localhost:1313/licenses/mit/ + https://example.org/licenses/mit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/licenses/mit/ + https://example.org/licenses/mit/ diff --git a/licenses/lgplv2/index.html b/licenses/lgplv2/index.html index b5b629c..e8db894 100644 --- a/licenses/lgplv2/index.html +++ b/licenses/lgplv2/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - Riss + + Riss [ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. diff --git a/licenses/lgplv2/index.xml b/licenses/lgplv2/index.xml index 610dc40..8991086 100644 --- a/licenses/lgplv2/index.xml +++ b/licenses/lgplv2/index.xml @@ -2,17 +2,17 @@ LGPLv2 on Formal Methods Tools - http://localhost:1313/licenses/lgplv2/ + https://example.org/licenses/lgplv2/ Recent content in LGPLv2 on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Riss - http://localhost:1313/tools/riss/ + https://example.org/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/riss/ + https://example.org/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 ee2671c..a655ccf 100644 --- a/licenses/mit/index.html +++ b/licenses/mit/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,76 @@ - - SMT-RAT + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … + + + + + + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + Colibri + Colibri is an SMT solver. + + + + + + + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … + + + + + + + Glucose + Glucose is a SAT solver. + + + + + + + + Lingeling + Lingeling is a SAT solver. + + + + + + + + MiniSat + [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … + + + + + + + Q3B + [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … + + + + + + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … @@ -90,8 +158,8 @@ APIs and Bindings This tool is available through the … - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -99,8 +167,8 @@ APIs and Bindings This tool is available … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/licenses/mit/index.xml b/licenses/mit/index.xml index e02dc89..35a6764 100644 --- a/licenses/mit/index.xml +++ b/licenses/mit/index.xml @@ -2,31 +2,87 @@ MIT on Formal Methods Tools - http://localhost:1313/licenses/mit/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/colibri/ + <p>Colibri is an SMT solver.</p> + + + CryptoMiniSat + https://example.org/tools/sat-smt/cryptominisat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/glucose/ + <p>Glucose is a SAT solver.</p> + + + Lingeling + https://example.org/tools/sat-smt/lingeling/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/lingeling/ + <p>Lingeling is a SAT solver.</p> + + + MiniSat + https://example.org/tools/sat-smt/minisat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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 1b8aab1..3ec8255 100644 --- a/maintenance/actively-maintained/index.html +++ b/maintenance/actively-maintained/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,85 @@ - - SMT-RAT + + Bitwuzla + Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … + + + + + + + Colibri + Colibri is an SMT solver. + + + + + + + + CryptoMiniSat + CryptoMiniSat is a SAT solver. +APIs and Bindings This tool is available through the following … + + + + + + + cvc5 + cvc5 is an automatic theorem prover for SMT problems. + + + + + + + + Glucose + Glucose is a SAT solver. + + + + + + + + Lingeling + Lingeling is a SAT solver. + + + + + + + + MathSAT + [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help … + + + + + + + OpenSMT + OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … + + + + + + + ParaFROST + ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … + + + + + + + SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the … @@ -90,8 +167,8 @@ APIs and Bindings This tool is available through the … - - SMTInterpol + + SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and … @@ -99,8 +176,8 @@ APIs and … - - STP + + STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available … @@ -108,24 +185,24 @@ APIs and Bindings This tool is available … - - veriT + + veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … - - Yices 2 + + Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the … - - Z3 + + Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This … diff --git a/maintenance/actively-maintained/index.xml b/maintenance/actively-maintained/index.xml index 678ffd4..e51ca6a 100644 --- a/maintenance/actively-maintained/index.xml +++ b/maintenance/actively-maintained/index.xml @@ -2,52 +2,115 @@ Actively Maintained on Formal Methods Tools - http://localhost:1313/maintenance/actively-maintained/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/colibri/ + <p>Colibri is an SMT solver.</p> + + + CryptoMiniSat + https://example.org/tools/sat-smt/cryptominisat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/cvc5/ + <p>cvc5 is an automatic theorem prover for SMT problems.</p> + + + Glucose + https://example.org/tools/sat-smt/glucose/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/glucose/ + <p>Glucose is a SAT solver.</p> + + + Lingeling + https://example.org/tools/sat-smt/lingeling/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/tools/sat-smt/lingeling/ + <p>Lingeling is a SAT solver.</p> + + + MathSAT + https://example.org/tools/sat-smt/mathsat/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + 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> + + + ParaFROST + https://example.org/tools/sat-smt/parafrost/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/smt-rat/ + https://example.org/tools/sat-smt/smt-rat/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smt-rat/ + https://example.org/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 - http://localhost:1313/tools/smtinterpol/ + https://example.org/tools/sat-smt/smtinterpol/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/smtinterpol/ + https://example.org/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 - http://localhost:1313/tools/stp/ + https://example.org/tools/sat-smt/stp/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/stp/ + https://example.org/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 - http://localhost:1313/tools/verit/ + https://example.org/tools/sat-smt/verit/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/verit/ + https://example.org/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 - http://localhost:1313/tools/yices/ + https://example.org/tools/sat-smt/yices/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/yices/ + https://example.org/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 - http://localhost:1313/tools/z3/ + https://example.org/tools/sat-smt/z3/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3/ + https://example.org/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/archived/index.xml b/maintenance/archived/index.xml deleted file mode 100644 index 1090225..0000000 --- a/maintenance/archived/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Archived on Formal Methods Tools - http://localhost:1313/maintenance/archived/ - Recent content in Archived on Formal Methods Tools - Hugo - en-us - Sat, 07 Jun 2025 00:00:00 +0000 - - - Riss - http://localhost:1313/tools/riss/ - Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/riss/ - <p>Riss is a SAT solving tool collection that was updated until 2017.</p> - - - diff --git a/maintenance/deprecated/index.xml b/maintenance/deprecated/index.xml deleted file mode 100644 index 5557b7a..0000000 --- a/maintenance/deprecated/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Deprecated on Formal Methods Tools - http://localhost:1313/maintenance/deprecated/ - Recent content in Deprecated on Formal Methods Tools - Hugo - en-us - Sat, 07 Jun 2025 00:00:00 +0000 - - - Riss - http://localhost:1313/tools/riss/ - Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/riss/ - <p>Riss is a SAT solving tool collection that was updated until 2017.</p> - - - diff --git a/maintenance/inactive/index.html b/maintenance/inactive/index.html deleted file mode 100644 index 117b6f8..0000000 --- a/maintenance/inactive/index.html +++ /dev/null @@ -1,104 +0,0 @@ - - - - - - - - -Inactive | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

- - - - - - - Inactive - -

- -
- - - - - - - - - - - - - - - - - - - - -
ToolDescription
SMTInterpolSMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. -APIs and …
- -
- - - diff --git a/maintenance/inactive/index.xml b/maintenance/inactive/index.xml deleted file mode 100644 index 3e0a5c8..0000000 --- a/maintenance/inactive/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Inactive on Formal Methods Tools - http://localhost:1313/maintenance/inactive/ - Recent content in Inactive on Formal Methods Tools - Hugo - en-us - Sat, 07 Jun 2025 00:00:00 +0000 - - - SMTInterpol - http://localhost:1313/tools/smtinterpol/ - Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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/maintenance/index.html b/maintenance/index.html index d8e6235..4d83433 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 110dd90..b99557d 100644 --- a/maintenance/index.xml +++ b/maintenance/index.xml @@ -2,24 +2,24 @@ Maintenance on Formal Methods Tools - http://localhost:1313/maintenance/ + https://example.org/maintenance/ Recent content in Maintenance on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + Actively Maintained - http://localhost:1313/maintenance/actively-maintained/ + https://example.org/maintenance/actively-maintained/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/maintenance/actively-maintained/ + https://example.org/maintenance/actively-maintained/ Not Maintained - http://localhost:1313/maintenance/not-maintained/ + https://example.org/maintenance/not-maintained/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/maintenance/not-maintained/ + https://example.org/maintenance/not-maintained/ diff --git a/maintenance/no-longer-maintained/index.html b/maintenance/no-longer-maintained/index.html deleted file mode 100644 index 827e4af..0000000 --- a/maintenance/no-longer-maintained/index.html +++ /dev/null @@ -1,104 +0,0 @@ - - - - - - - - -No Longer Maintained | Formal Methods Tools - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-

Formal Methods Tools

- - - - -
-
- -

- - - - - - - No Longer Maintained - -

- -
- - - - - - - - - - - - - - - - - - - - -
ToolDescription
Riss No Longer Maintained Riss is a SAT solving tool collection that was updated until 2017. -
- -
- - - diff --git a/maintenance/no-longer-maintained/index.xml b/maintenance/no-longer-maintained/index.xml deleted file mode 100644 index b73ccc8..0000000 --- a/maintenance/no-longer-maintained/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - No Longer Maintained on Formal Methods Tools - http://localhost:1313/maintenance/no-longer-maintained/ - Recent content in No Longer Maintained on Formal Methods Tools - Hugo - en-us - Sat, 07 Jun 2025 00:00:00 +0000 - - - Riss - http://localhost:1313/tools/riss/ - Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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(226, 59, 59);"></span> <span style="color: rgb(226, 59, 59); font-size: 1rem;">No Longer Maintained</span> </div> Riss is a SAT solving tool collection that was updated until 2017.</p> - - - diff --git a/maintenance/not-active/index.xml b/maintenance/not-active/index.xml deleted file mode 100644 index 05d0630..0000000 --- a/maintenance/not-active/index.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - Not Active on Formal Methods Tools - http://localhost:1313/maintenance/not-active/ - Recent content in Not Active on Formal Methods Tools - Hugo - en-us - Sat, 07 Jun 2025 00:00:00 +0000 - - - Riss - http://localhost:1313/tools/riss/ - Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/riss/ - <p>Riss is a SAT solving tool collection that was updated until 2017.</p> - - - diff --git a/maintenance/not-maintained/index.html b/maintenance/not-maintained/index.html index db89d1a..d0f7a7d 100644 --- a/maintenance/not-maintained/index.html +++ b/maintenance/not-maintained/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,9 +81,50 @@ - - Riss - Not Maintained Since {map[year:2017] /home/landon/gitea/fmtools/content/tools/riss.md <nil> … + + Boolector + [ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … + + + + + + + cvc4 + [ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … + + + + + + + dReal + [ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems … + + + + + + + MiniSat + [ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … + + + + + + + Q3B + [ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … + + + + + + + Riss + [ Not Maintained Since 2017 ] Riss is a SAT solving tool collection. + diff --git a/maintenance/not-maintained/index.xml b/maintenance/not-maintained/index.xml index b9b6e45..635b8da 100644 --- a/maintenance/not-maintained/index.xml +++ b/maintenance/not-maintained/index.xml @@ -2,18 +2,53 @@ Not Maintained on Formal Methods Tools - http://localhost:1313/maintenance/not-maintained/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/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 - http://localhost:1313/tools/riss/ + https://example.org/tools/sat-smt/riss/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/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(226, 59, 59);"></span> <span style="color: rgb(226, 59, 59); font-size: 1rem;">Not Maintained Since {map[year:2017] /home/landon/gitea/fmtools/content/tools/riss.md &lt;nil&gt; inactive true 0 {{} {{} 0} {{} {0 0}}} {{} {{} 0} {{} {0 0}}} 615 { 0 0 0} &lt;nil&gt;}</span> </div> Riss is a SAT solving tool collection that was updated until 2017.</p> + https://example.org/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 978acb3..d67473e 100644 --- a/privacy/index.html +++ b/privacy/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -66,10 +66,10 @@
-

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

-

If you choose to contribute content (such as submitting an article or comment), any information you voluntarily provide will be stored as part of the website’s content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website’s owner. Any information you voluntarily provide as part of a code contribution becomes public information and may be used by the general public as allowed by respective laws and policies.

-

Your privacy is respected, and no unnecessary data is collected or shared. If you or your tool is listed on this page and you would like to remove it, please contact fmtools@mossbiscuits.com with the subject Please remove my data.

-

Look at you, reading privacy policies. Thanks for being a responsible internet user.

+

This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and there is no money to be made from this project.

+

If you choose to contribute content (including emails, issues, and pull requests), any information you voluntarily provide may be stored as part of the website’s content and source code. Only the data you explicitly submit will be saved, and data is not sold by the website’s owner. Due to the public nature of its disclosure, this information is not considered private and may be used by the general public as allowed by respective laws and policies. Your privacy is respected, and no unnecessary data is collected or shared.

+

If your information (e.g., your name, a tool you developed, or an attribution) is listed on this website and you would like to remove it, please contact fmtools@mossbiscuits.com with the subject Please remove my data. I cannot make guarantees, but I will make a reasonable effort to remove or redact your information within 1-3 business days.

+

Look at you, reading privacy policies. Thanks for being a responsible internet user. Now go do something more interesting 🙂

diff --git a/sitemap.xml b/sitemap.xml index 177fbf4..0388399 100644 --- a/sitemap.xml +++ b/sitemap.xml @@ -2,147 +2,268 @@ - http://localhost:1313/interfaces/.net/ + https://example.org/interfaces/.net/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/maintenance/actively-maintained/ + https://example.org/maintenance/actively-maintained/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/ + https://example.org/developers/albert-ludwigs-universit%C3%A4t/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/applications/ + https://example.org/tools/pmc/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/licenses/bsd/ + https://example.org/licenses/all-rights-reserved/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/c/ + https://example.org/tools/sat-smt/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/c++/ + https://example.org/tools/termination/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/cli/ + https://example.org/tools/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/applications/constraint-solver/ + https://example.org/licenses/apache-2.0/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/ + https://example.org/applications/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/inputs/dimacs/ + https://example.org/tools/sat-smt/bitwuzla/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/licenses/gplv3/ + https://example.org/tools/sat-smt/boolector/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/inputs/ + https://example.org/licenses/bsd/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/ + https://example.org/interfaces/c/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/java/ + https://example.org/interfaces/c++/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/licenses/ + https://example.org/techniques/cdcl/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/loria/ + https://example.org/developers/cea/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/maintenance/ + https://example.org/interfaces/cli/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/microsoft-research/ + https://example.org/inputs/cnf/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/licenses/mit/ + https://example.org/tools/sat-smt/colibri/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/maintenance/not-maintained/ + https://example.org/applications/constraint-solver/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/online/ + https://example.org/tools/sat-smt/cryptominisat/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/python/ + https://example.org/tools/sat-smt/cvc4/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/riss/ + https://example.org/tools/sat-smt/cvc5/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/interfaces/rust/ + https://example.org/developers/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/rwth-aachen/ + https://example.org/inputs/dimacs/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/applications/sat-solver/ + https://example.org/developers/disi-university-of-trento/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/applications/smt-solver/ + https://example.org/tools/sat-smt/dreal/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/smt-rat/ + https://example.org/developers/eindhoven-university-of-technology/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/smtinterpol/ + https://example.org/developers/fondazione-bruno-kessler/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/inputs/smtlib2/ + https://example.org/developers/gilles-audemard/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/sri-international/ + https://example.org/tools/sat-smt/glucose/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/stanford-university/ + https://example.org/licenses/gplv2/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/stp/ + https://example.org/licenses/gplv3/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/ + https://example.org/techniques/gpu/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/applications/theorem-prover/ + https://example.org/inputs/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/uliege/ + https://example.org/developers/inria-rh%C3%B4ne-alpes/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/university-of-freiburg/ + https://example.org/interfaces/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/developers/university-of-illinois/ + https://example.org/interfaces/java/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/verit/ + https://example.org/developers/johannes-kepler-universit%C3%A4t-linz/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/inputs/yices-2/ + https://example.org/developers/laurent-simon/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/yices/ + https://example.org/licenses/lgplv2/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/tools/z3/ + https://example.org/licenses/ 2025-06-07T00:00:00+00:00 - http://localhost:1313/about/ + https://example.org/tools/sat-smt/lingeling/ + 2025-06-07T00:00:00+00:00 - http://localhost:1313/taxonomies/ + https://example.org/developers/loria/ + 2025-06-07T00:00:00+00:00 - http://localhost:1313/contribute/ + https://example.org/maintenance/ + 2025-06-07T00:00:00+00:00 - http://localhost:1313/domains/ + https://example.org/developers/masaryk-university/ + 2025-06-07T00:00:00+00:00 - http://localhost:1313/license/ + https://example.org/tools/sat-smt/mathsat/ + 2025-06-07T00:00:00+00:00 - http://localhost:1313/privacy/ + https://example.org/developers/microsoft-research/ + 2025-06-07T00:00:00+00:00 - http://localhost:1313/techniques/ + https://example.org/tools/sat-smt/minisat/ + 2025-06-07T00:00:00+00:00 + + https://example.org/licenses/mit/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/niklas-e%C3%A9n/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/niklas-s%C3%B6rensson/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/norbert-manthey/ + 2025-06-07T00:00:00+00:00 + + https://example.org/maintenance/not-maintained/ + 2025-06-07T00:00:00+00:00 + + https://example.org/interfaces/online/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/opensmt/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/parafrost/ + 2025-06-07T00:00:00+00:00 + + https://example.org/interfaces/python/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/q3b/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/riss/ + 2025-06-07T00:00:00+00:00 + + https://example.org/interfaces/rust/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/rwth-aachen/ + 2025-06-07T00:00:00+00:00 + + https://example.org/applications/sat-solver/ + 2025-06-07T00:00:00+00:00 + + https://example.org/applications/smt-solver/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/smt-rat/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/smtinterpol/ + 2025-06-07T00:00:00+00:00 + + https://example.org/inputs/smtlib2/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/sri-international/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/stanford-university/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/stp/ + 2025-06-07T00:00:00+00:00 + + https://example.org/techniques/ + 2025-06-07T00:00:00+00:00 + + https://example.org/ + 2025-06-07T00:00:00+00:00 + + https://example.org/applications/theorem-prover/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/uliege/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/university-of-freiburg/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/university-of-illinois/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/university-of-iowa/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/university-of-lugano/ + 2025-06-07T00:00:00+00:00 + + https://example.org/developers/university-of-virginia/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/verit/ + 2025-06-07T00:00:00+00:00 + + https://example.org/inputs/yices-2/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/yices/ + 2025-06-07T00:00:00+00:00 + + https://example.org/tools/sat-smt/z3/ + 2025-06-07T00:00:00+00:00 + + https://example.org/about/ + + https://example.org/taxonomies/ + + https://example.org/contribute/ + + https://example.org/domains/ + + https://example.org/license/ + + https://example.org/privacy/ diff --git a/taxonomies/index.html b/taxonomies/index.html index e59316c..1b52e0d 100644 --- a/taxonomies/index.html +++ b/taxonomies/index.html @@ -1,6 +1,6 @@ - + @@ -15,16 +15,16 @@ - + - + - - - - + + + + - + @@ -171,6 +171,159 @@ the tools developed at SRI International).

+ + Albert-Ludwigs-Universität + + + + + + + + + + + + + CEA + + + + + + + + + + + + + DISI-University of Trento + + + + + + + + + + + + + Eindhoven University of Technology + + + + + + + + + + + + + Fondazione Bruno Kessler + + + + + + + + + + + + + Gilles Audemard + + + + + + + + + + + + + INRIA Rhône-Alpes + + + + + + + + + + + + + Johannes Kepler Universität Linz + + + + + + + + + + + + + Laurent Simon + + + + + + + + + + + + + Niklas Eén + + + + + + + + + + + + + Niklas Sörensson + + + + + + + + + + + + + + + + + + + + + University of Iowa + + + + + + + + + + + + + University of Lugano + + + + + + + + + + + + + University of Virginia + + + @@ -358,6 +596,23 @@ the tools developed at SRI International).

+ + CNF + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + GPLv2 + + + + + + + + + + + + + + + Techniques + + + + + + + + + + + + + + CDCL + + + + + + + + + + + + + GPU + + + + + + diff --git a/taxonomies/index.xml b/taxonomies/index.xml index 02bdae5..19d5fe8 100644 --- a/taxonomies/index.xml +++ b/taxonomies/index.xml @@ -2,10 +2,10 @@ All Taxonomy Data on Formal Methods Tools - http://localhost:1313/taxonomies/ + https://example.org/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 9bfa3d1..a5a77cf 100644 --- a/techniques/cdcl/index.html +++ b/techniques/cdcl/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - ParaFROST + + ParaFROST ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … diff --git a/techniques/cdcl/index.xml b/techniques/cdcl/index.xml index b40aff4..8f1909f 100644 --- a/techniques/cdcl/index.xml +++ b/techniques/cdcl/index.xml @@ -2,17 +2,17 @@ CDCL on Formal Methods Tools - http://localhost:1313/techniques/cdcl/ + https://example.org/techniques/cdcl/ Recent content in CDCL on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + ParaFROST - http://localhost:1313/tools/z3-copy/ + https://example.org/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3-copy/ + https://example.org/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 5f2da6f..6fea698 100644 --- a/techniques/gpu/index.html +++ b/techniques/gpu/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -81,8 +81,8 @@ - - ParaFROST + + ParaFROST ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … diff --git a/techniques/gpu/index.xml b/techniques/gpu/index.xml index 695d32c..5d52b2e 100644 --- a/techniques/gpu/index.xml +++ b/techniques/gpu/index.xml @@ -2,17 +2,17 @@ GPU on Formal Methods Tools - http://localhost:1313/techniques/gpu/ + https://example.org/techniques/gpu/ Recent content in GPU on Formal Methods Tools Hugo en-us Sat, 07 Jun 2025 00:00:00 +0000 - + ParaFROST - http://localhost:1313/tools/z3-copy/ + https://example.org/tools/sat-smt/parafrost/ Sat, 07 Jun 2025 00:00:00 +0000 - http://localhost:1313/tools/z3-copy/ + https://example.org/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 2af0b03..1e74fa0 100644 --- a/techniques/index.html +++ b/techniques/index.html @@ -1,6 +1,6 @@ - + @@ -14,16 +14,16 @@ - + - + - - - - + + + + - + @@ -61,6 +61,42 @@
+ + + + + + + + + + + CDCL + + + + + + + + + + + + + + GPU + + +
diff --git a/techniques/index.xml b/techniques/index.xml index 0ec9808..92394f1 100644 --- a/techniques/index.xml +++ b/techniques/index.xml @@ -2,10 +2,25 @@ Techniques on Formal Methods Tools - http://localhost:1313/techniques/ + https://example.org/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/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/techniques/cdcl/ + + + + GPU + https://example.org/techniques/gpu/ + Sat, 07 Jun 2025 00:00:00 +0000 + https://example.org/techniques/gpu/ + + diff --git a/tools/index.html b/tools/index.html index ea537e4..18c4566 100644 --- a/tools/index.html +++ b/tools/index.html @@ -1,6 +1,6 @@ - + @@ -16,16 +16,16 @@ - + - + - - - - + + + + - + @@ -58,6 +58,70 @@ Click a colorful item in the">
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

All Tools

This page lists all of the tools on this site in alphabetical order. Click a tool name in the first column to view tool details. @@ -66,69 +130,40 @@ Item colors mean nothing and are intended to make it easy to skim the page. Colors are generated by hashing each term’s name and converting it to RGB color values.

+ + + + + + + + - - + + - - + @@ -136,191 +171,9 @@ Colors are generated by hashing each term’s name and converting it to RGB - - - - - - - - - - - - - - - - Gilles Audemard - - - - - - - - - - - - - Laurent Simon - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + - - + + +
ToolApplicationsDevelopersLicense
Glucose
- - - - - - - - - - - - - SAT Solver - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + Bitwuzla
Lingeling - - - - - - - - - - - - - - - SAT Solver - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Johannes Kepler Universität Linz - - - - - - - - - - - - - - - - - - - - - - - - - - -
MathSAT - - - - - - + + + @@ -336,46 +189,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + @@ -385,66 +200,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - Fondazione Bruno Kessler + id="applications_theorem-prover" + style="background:rgba(190,35,109,0.4)" + href="/applications/theorem-prover"> + Theorem Prover - - - - - - - - - - - DISI-University of Trento - - - - - - - - - - - - - - - - - - - - - - - - - - -
MiniSat - - - - - - + + @@ -460,8 +223,12 @@ Colors are generated by hashing each term’s name and converting it to RGB SAT Solver - - + + + + + + @@ -497,9 +264,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -509,39 +288,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - Niklas Eén + id="licenses_mit" + style="background:rgba(122,188,26,0.4)" + href="/licenses/mit"> + MIT - - - - - - - - - - - Niklas Sörensson - - - - - - - - - - - - + + @@ -560,15 +314,24 @@ Colors are generated by hashing each term’s name and converting it to RGB
OpenSMT
+ + +
+ Boolector + +
+ + + 		- - - + + + @@ -584,48 +347,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + @@ -635,51 +358,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - University of Lugano + id="applications_theorem-prover" + style="background:rgba(190,35,109,0.4)" + href="/applications/theorem-prover"> + Theorem Prover - - - - - - - - - - - - - - - - - - - - - - - - - - -
ParaFROST - - - - - - + + @@ -695,10 +381,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SAT Solver - - - - + + @@ -738,9 +422,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -750,45 +446,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - Eindhoven University of Technology + id="licenses_mit" + style="background:rgba(122,188,26,0.4)" + href="/licenses/mit"> + MIT - - - - - - - - - - - Albert-Ludwigs-Universität - - - - - - - - - - - - - - - - - - + + @@ -807,15 +472,21 @@ Colors are generated by hashing each term’s name and converting it to RGB
Q3B
+ + + Colibri + + + - - - + + + @@ -831,10 +502,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - - - - + + @@ -872,9 +541,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -884,28 +565,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - Masaryk University + id="licenses_mit" + style="background:rgba(122,188,26,0.4)" + href="/licenses/mit"> + MIT - - - - - - - - - - - - - - - - + + @@ -922,15 +589,21 @@ Colors are generated by hashing each term’s name and converting it to RGB
Riss
+ + + CryptoMiniSat + + + - - - + + + @@ -946,8 +619,10 @@ Colors are generated by hashing each term’s name and converting it to RGB SAT Solver - - + + + + @@ -985,9 +660,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -997,24 +684,31 @@ Colors are generated by hashing each term’s name and converting it to RGB - Norbert Manthey + id="licenses_mit" + style="background:rgba(122,188,26,0.4)" + href="/licenses/mit"> + MIT - - - - - - - - - - - - + + + + + + + + + + + GPLv2 + + + + @@ -1033,15 +727,24 @@ Colors are generated by hashing each term’s name and converting it to RGB
SMT-RAT
+ + +
+ cvc4 + +
+ + + 		- - - + + + @@ -1057,8 +760,379 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - + + + + + + + + + + + Theorem Prover + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + +
+ + + cvc5 + + + + + + + + + + + + + + + + + + SMT Solver + + + + + + + + + + + + + Theorem Prover + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + BSD + + + + + + + + + + + + + + + + + + +
+ + +
+ dReal + +
+ + + 		+ + + + + + + + + + + + + + + SMT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Apache-2.0 + + + + + + + + + + + + + + + + +
+ + + Glucose + + + + + + + + + @@ -1074,10 +1148,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SAT Solver - - - - + + @@ -1115,9 +1187,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -1127,28 +1211,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - RWTH Aachen + id="licenses_mit" + style="background:rgba(122,188,26,0.4)" + href="/licenses/mit"> + MIT - - - - - - - - - - - - - - - - + + @@ -1165,15 +1235,134 @@ Colors are generated by hashing each term’s name and converting it to RGB
SMTInterpol
+ + + Lingeling + + + - - + + + + + + + + + + + + SAT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + +
+ + + MathSAT + + + + + + + + + @@ -1189,8 +1378,356 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + All Rights Reserved + + + + + + + + + + + + + + + + +
+ + +
+ MiniSat + +
+ + + 		+ + + + + + + + + + + + + + + SAT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + +
+ + + OpenSMT + + + + + + + + + + + + + + + + + + SMT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + +
+ + + ParaFROST + + + + + + + + + + + + + + + + + + SAT Solver + + + + + + @@ -1230,9 +1767,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -1242,24 +1791,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - University of Freiburg + id="licenses_gplv3" + style="background:rgba(182,14,173,0.4)" + href="/licenses/gplv3"> + GPLv3 - - - - - - - - - - - - + + @@ -1280,15 +1819,524 @@ Colors are generated by hashing each term’s name and converting it to RGB
STP
+ + +
+ Q3B + +
+ + + 		- - + + + + + + + + + + + + SMT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + +
+ + +
+ Riss + +
+ + + 		+ + + + + + + + + + + + + + + SAT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + LGPLv2 + + + + + + + + + + + + + + + + +
+ + + SMT-RAT + + + + + + + + + + + + + + + + + + SMT Solver + + + + + + + + + + + + + SAT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + MIT + + + + + + + + + + + + + + + + + + +
+ + + SMTInterpol + + + + + + + + + + + + + + + + + + SMT Solver + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GPLv3 + + + + + + + + + + + + + + + + + + +
+ + + STP + + + + + + + + + @@ -1304,8 +2352,8 @@ Colors are generated by hashing each term’s name and converting it to RGB Constraint Solver - - + + @@ -1321,8 +2369,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - - + + @@ -1338,8 +2386,8 @@ Colors are generated by hashing each term’s name and converting it to RGB Theorem Prover - - + + @@ -1379,9 +2427,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -1391,43 +2451,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - University of Illinois + id="licenses_mit" + style="background:rgba(122,188,26,0.4)" + href="/licenses/mit"> + MIT - - - - - - - - - - - Stanford University - - - - - - - - - - - - - - - - + + @@ -1446,15 +2477,21 @@ Colors are generated by hashing each term’s name and converting it to RGB
veriT
+ + + veriT + + + - - - + + + @@ -1470,8 +2507,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - - + + @@ -1511,9 +2548,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -1523,43 +2572,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - LORIA + id="licenses_bsd" + style="background:rgba(197,57,224,0.4)" + href="/licenses/bsd"> + BSD - - - - - - - - - - - ULiege - - - - - - - - - - - - - - - - + + @@ -1578,15 +2598,21 @@ Colors are generated by hashing each term’s name and converting it to RGB
Yices 2
+ + + Yices 2 + + + - - - + + + @@ -1602,8 +2628,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - - + + @@ -1619,8 +2645,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SAT Solver - - + + @@ -1660,9 +2686,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -1672,26 +2710,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - SRI International + id="licenses_gplv3" + style="background:rgba(182,14,173,0.4)" + href="/licenses/gplv3"> + GPLv3 - - - - - - - - - - - - - - + + @@ -1710,15 +2736,21 @@ Colors are generated by hashing each term’s name and converting it to RGB
Z3
+ + + Z3 + + + - - - + + + @@ -1734,8 +2766,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SMT Solver - - + + @@ -1751,8 +2783,8 @@ Colors are generated by hashing each term’s name and converting it to RGB Theorem Prover - - + + @@ -1768,8 +2800,8 @@ Colors are generated by hashing each term’s name and converting it to RGB SAT Solver - - + + @@ -1809,9 +2841,21 @@ Colors are generated by hashing each term’s name and converting it to RGB - - + + + + + + + + + + + + + + @@ -1821,26 +2865,14 @@ Colors are generated by hashing each term’s name and converting it to RGB - Microsoft Research + id="licenses_mit" + style="background:rgba(122,188,26,0.4)" + href="/licenses/mit"> + MIT - - - - - - - - - - - - - - + + @@ -1859,9 +2891,16 @@ Colors are generated by hashing each term’s name and converting it to RGB
+
+ + Black dot indicates tool has not been maintained recently +
+ +