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
new file mode 100644
index 0000000..287caf1
--- /dev/null
+++ b/applications/sat-solver/index.xml
@@ -0,0 +1,47 @@
+
+
+
+ SAT Solver on Formal Methods Tools
+ http://localhost:1313/applications/sat-solver/
+ Recent content in SAT Solver on Formal Methods Tools
+ Hugo
+ en-us
+ Sat, 07 Jun 2025 00:00:00 +0000
+
+
+ ParaFROST
+ http://localhost:1313/tools/parafrost/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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(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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 b817193..3369ae3 100644
--- a/applications/smt-solver/index.html
+++ b/applications/smt-solver/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,44 @@
+
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 …
+
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
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 …
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the …
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 53d6bef..9120700 100644
--- a/applications/smt-solver/index.xml
+++ b/applications/smt-solver/index.xml
@@ -2,32 +2,60 @@
SMT Solver on Formal Methods Tools
- https://example.org/applications/smt-solver/
+ http://localhost:1313/applications/smt-solver/
Recent content in SMT Solver on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+
+
+ Q3B
+ http://localhost:1313/tools/q3b/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.</p>Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 c4283d6..5342884 100644
--- a/applications/theorem-prover/index.html
+++ b/applications/theorem-prover/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,19 @@
+
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
+APIs and Bindings This …
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 …
+
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 b2abb5f..db30ec1 100644
--- a/developers/loria/index.xml
+++ b/developers/loria/index.xml
@@ -2,17 +2,17 @@
LORIA on Formal Methods Tools
- https://example.org/developers/loria/
+ http://localhost:1313/developers/loria/
Recent content in LORIA on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/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
new file mode 100644
index 0000000..6f6d65a
--- /dev/null
+++ b/developers/masaryk-university/index.html
@@ -0,0 +1,103 @@
+
+
+
+
+
+
+
+
+Masaryk University | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 5b3e7c6..b4e9b8b 100644
--- a/developers/microsoft-research/index.xml
+++ b/developers/microsoft-research/index.xml
@@ -2,18 +2,18 @@
Microsoft Research on Formal Methods Tools
- https://example.org/developers/microsoft-research/
+ http://localhost:1313/developers/microsoft-research/
Recent content in Microsoft Research on Formal Methods ToolsHugoen-us
- Fri, 02 Feb 2024 04:14:54 -0800
-
+ Sat, 07 Jun 2025 00:00:00 +0000
+ Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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
new file mode 100644
index 0000000..e07af04
--- /dev/null
+++ b/developers/niklas-eén/index.html
@@ -0,0 +1,103 @@
+
+
+
+
+
+
+
+
+Niklas Eén | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
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 …
+
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 a47e9c1..9d32cec 100644
--- a/developers/sri-international/index.xml
+++ b/developers/sri-international/index.xml
@@ -2,18 +2,18 @@
SRI International on Formal Methods Tools
- https://example.org/developers/sri-international/
+ http://localhost:1313/developers/sri-international/
Recent content in SRI International on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/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
new file mode 100644
index 0000000..7cdb8b2
--- /dev/null
+++ b/developers/stanford-university/index.html
@@ -0,0 +1,104 @@
+
+
+
+
+
+
+
+
+Stanford University | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
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 …
+
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 8e9d060..9660980 100644
--- a/developers/uliege/index.xml
+++ b/developers/uliege/index.xml
@@ -2,17 +2,17 @@
ULiege on Formal Methods Tools
- https://example.org/developers/uliege/
+ http://localhost:1313/developers/uliege/
Recent content in ULiege on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/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
new file mode 100644
index 0000000..9d92152
--- /dev/null
+++ b/developers/university-of-freiburg/index.html
@@ -0,0 +1,112 @@
+
+
+
+
+
+
+
+
+University of Freiburg | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
-Z3 …
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 …
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas …
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 …
+
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal …
+ Glucose
+
+
diff --git a/index.xml b/index.xml
index f4c3ca5..ccf093e 100644
--- a/index.xml
+++ b/index.xml
@@ -2,59 +2,136 @@
The Ultimate Formal Methods Toolbox on Formal Methods Tools
- https://example.org/
+ http://localhost:1313/
Recent content in The Ultimate Formal Methods Toolbox on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+
+
+ Glucose
+ http://localhost:1313/tools/glucose/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/glucose/
+ <p>Glucose is a SAT solver.</p>
+
+
+ Lingeling
+ http://localhost:1313/tools/lingeling/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/lingeling/
+ <p>Lingeling is a SAT solver.</p>
+
+
+ MathSAT
+ http://localhost:1313/tools/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(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">] </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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ ParaFROST
+ http://localhost:1313/tools/parafrost/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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(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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.</p>Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html">Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">Z3 C++ Namespace Reference</a></li>
<li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html">Z3 .NET Namespace Reference</a></li>
<li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html">Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li>
</ul>About
- https://example.org/about/
+ http://localhost:1313/about/
Mon, 01 Jan 0001 00:00:00 +0000
- https://example.org/about/
+ http://localhost:1313/about/<p>The Formal Methods Tools project is dedicated to developing, maintaining, and promoting tools that support the application of formal methods in software engineering. Our goal is to make formal verification, specification, and analysis techniques accessible and practical for both researchers and practitioners.</p>
<h2 id="key-objectives">Key Objectives</h2>
<ul>
<li>Provide a comprehensive list of tools for formal methods.</li>
<li>Group tools by rich metadata to support collaboration and boost tools’ strengths.</li>
<li>Foster a collaborative community for tool development and support.</li>
</ul>
<h2 id="whos-behind-this">Who’s Behind This?</h2>
<p>Howdy. My name is Landon Taylor. I sometimes go by mossBiscuits.
This is one of my hobby projects.
I have a passion for formal methods. When I started learning about verification, there was a sharp barrier to entry due partially to the sprawl of content online.
I wanted to solve this problem, so I have been chipping away at this website for a while now.</p>Contribute
- https://example.org/contribute/
+ http://localhost:1313/contribute/
Mon, 01 Jan 0001 00:00:00 +0000
- https://example.org/contribute/
+ http://localhost:1313/contribute/<p>Instructions coming soon. Please see <a href="https://gitmoss.fyi/fmtools/content/wiki/Contribute">https://gitmoss.fyi/fmtools/content/wiki/Contribute</a> for temporary instructions.</p>MIT License
- https://example.org/license/
+ http://localhost:1313/license/
Mon, 01 Jan 0001 00:00:00 +0000
- https://example.org/license/
+ http://localhost:1313/license/<p>MIT License</p>
<p>Copyright (c) 2025 Landon Taylor.</p>
<p>Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:</p>Privacy
- https://example.org/privacy/
+ http://localhost:1313/privacy/
Mon, 01 Jan 0001 00:00:00 +0000
- https://example.org/privacy/
+ http://localhost:1313/privacy/<p>This website does not collect or track any personal data from visitors. No cookies, personalized analytics, or tracking scripts are used. No ads are shown on this website, and</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’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.</p>
diff --git a/inputs/cnf/index.html b/inputs/cnf/index.html
new file mode 100644
index 0000000..24e6049
--- /dev/null
+++ b/inputs/cnf/index.html
@@ -0,0 +1,104 @@
+
+
+
+
+
+
+
+
+CNF | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
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 …
+
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 2df32c0..8fc7f84 100644
--- a/inputs/dimacs/index.xml
+++ b/inputs/dimacs/index.xml
@@ -2,25 +2,25 @@
DIMACS on Formal Methods Tools
- https://example.org/inputs/dimacs/
+ http://localhost:1313/inputs/dimacs/
Recent content in DIMACS on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.</p>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 4fa623c..1e30ce3 100644
--- a/inputs/index.html
+++ b/inputs/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
diff --git a/inputs/index.xml b/inputs/index.xml
index bd2bbce..94f041c 100644
--- a/inputs/index.xml
+++ b/inputs/index.xml
@@ -2,31 +2,31 @@
Inputs on Formal Methods Tools
- https://example.org/inputs/
+ http://localhost:1313/inputs/
Recent content in Inputs on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ DIMACS
- https://example.org/inputs/dimacs/
+ http://localhost:1313/inputs/dimacs/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/inputs/dimacs/
+ http://localhost:1313/inputs/dimacs/SMTLIB2
- https://example.org/inputs/smtlib2/
+ http://localhost:1313/inputs/smtlib2/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/inputs/smtlib2/
+ http://localhost:1313/inputs/smtlib2/Yices 2
- https://example.org/inputs/yices-2/
+ http://localhost:1313/inputs/yices-2/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/inputs/yices-2/
+ http://localhost:1313/inputs/yices-2/
diff --git a/inputs/smtlib2/index.html b/inputs/smtlib2/index.html
index 3e7c0d0..7761ccc 100644
--- a/inputs/smtlib2/index.html
+++ b/inputs/smtlib2/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,36 @@
+
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 …
+
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
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 …
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the …
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 39beae1..3e19112 100644
--- a/inputs/smtlib2/index.xml
+++ b/inputs/smtlib2/index.xml
@@ -2,32 +2,53 @@
SMTLIB2 on Formal Methods Tools
- https://example.org/inputs/smtlib2/
+ http://localhost:1313/inputs/smtlib2/
Recent content in SMTLIB2 on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+
+
+ SMT-RAT
+ http://localhost:1313/tools/smt-rat/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.</p>Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 56d5f8b..1f45235 100644
--- a/inputs/yices-2/index.html
+++ b/inputs/yices-2/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -83,7 +83,7 @@
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 …
+
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 db0f0e4..86c15a3 100644
--- a/inputs/yices-2/index.xml
+++ b/inputs/yices-2/index.xml
@@ -2,18 +2,18 @@
Yices 2 on Formal Methods Tools
- https://example.org/inputs/yices-2/
+ http://localhost:1313/inputs/yices-2/
Recent content in Yices 2 on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/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 a62eb2e..ec56323 100644
--- a/interfaces/.net/index.html
+++ b/interfaces/.net/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -83,7 +83,8 @@
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 ee25e15..040e11d 100644
--- a/interfaces/.net/index.xml
+++ b/interfaces/.net/index.xml
@@ -2,18 +2,18 @@
.NET on Formal Methods Tools
- https://example.org/interfaces/.net/
+ http://localhost:1313/interfaces/.net/
Recent content in .NET on Formal Methods ToolsHugoen-us
- Fri, 02 Feb 2024 04:14:54 -0800
-
+ Sat, 07 Jun 2025 00:00:00 +0000
+ Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 67cc1d4..b7126e4 100644
--- a/interfaces/c++/index.html
+++ b/interfaces/c++/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,19 @@
+
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 7f6f9cd..03c18b2 100644
--- a/interfaces/c++/index.xml
+++ b/interfaces/c++/index.xml
@@ -2,18 +2,25 @@
C++ on Formal Methods Tools
- https://example.org/interfaces/c++/
+ http://localhost:1313/interfaces/c++/
Recent content in C++ on Formal Methods ToolsHugoen-us
- Fri, 02 Feb 2024 04:14:54 -0800
-
+ Sat, 07 Jun 2025 00:00:00 +0000
+
+
+ SMT-RAT
+ http://localhost:1313/tools/smt-rat/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/smt-rat/
+ <p>SMT-RAT is an SMT Real Algebra Toolbox.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C++ API:</strong> <a href="https://ths-rwth.github.io/smtrat/dc/dad/md__builds_ths_smt_smtrat_doc_markdown_07_using_smtrat.html#autotoc_md25">C++ API Reference</a></li>
</ul>
+ Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 19404f0..0dc0b4c 100644
--- a/interfaces/c/index.html
+++ b/interfaces/c/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,19 @@
+
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 57551c1..4f72437 100644
--- a/interfaces/c/index.xml
+++ b/interfaces/c/index.xml
@@ -2,18 +2,25 @@
C on Formal Methods Tools
- https://example.org/interfaces/c/
+ http://localhost:1313/interfaces/c/
Recent content in C on Formal Methods ToolsHugoen-us
- Fri, 02 Feb 2024 04:14:54 -0800
-
+ Sat, 07 Jun 2025 00:00:00 +0000
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 f1f00dd..c528384 100644
--- a/interfaces/cli/index.html
+++ b/interfaces/cli/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,44 @@
+
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 …
+
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
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 …
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the …
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 13e829f..0d13662 100644
--- a/interfaces/cli/index.xml
+++ b/interfaces/cli/index.xml
@@ -2,32 +2,60 @@
CLI on Formal Methods Tools
- https://example.org/interfaces/cli/
+ http://localhost:1313/interfaces/cli/
Recent content in CLI on Formal Methods ToolsHugoen-usSat, 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 <nil> inactive true 0 {{} {{} 0} {{} {0 0}}} {{} {{} 0} {{} {0 0}}} 615 { 0 0 0} <nil>}</span>
</div>
Riss is a SAT solving tool collection that was updated until 2017.</p>
+
+
+ SMT-RAT
+ http://localhost:1313/tools/smt-rat/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.</p>Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 141a9b8..abf249a 100644
--- a/interfaces/index.html
+++ b/interfaces/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -70,60 +70,6 @@
-
- CLI
-
-
-
-
-
-
-
-
-
-
-
-
-
- Python
-
-
-
-
-
-
-
-
-
-
-
-
-
- Rust
-
-
-
-
-
-
-
-
-
-
-
-
+ CLI
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Python
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Rust
+
+
+
diff --git a/interfaces/index.xml b/interfaces/index.xml
index af6c0f6..43838fd 100644
--- a/interfaces/index.xml
+++ b/interfaces/index.xml
@@ -2,66 +2,66 @@
Interfaces on Formal Methods Tools
- https://example.org/interfaces/
+ http://localhost:1313/interfaces/
Recent content in Interfaces on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
-
- CLI
- https://example.org/interfaces/cli/
- Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/interfaces/cli/
-
-
-
- Python
- https://example.org/interfaces/python/
- Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/interfaces/python/
-
-
-
- Rust
- https://example.org/interfaces/rust/
- Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/interfaces/rust/
-
-
+ .NET
- https://example.org/interfaces/.net/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/interfaces/.net/
+ http://localhost:1313/interfaces/.net/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/.net/C
- https://example.org/interfaces/c/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/interfaces/c/
+ http://localhost:1313/interfaces/c/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/c/C++
- https://example.org/interfaces/c++/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/interfaces/c++/
+ http://localhost:1313/interfaces/c++/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/c++/
+
+
+
+ CLI
+ http://localhost:1313/interfaces/cli/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/cli/Java
- https://example.org/interfaces/java/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/interfaces/java/
+ http://localhost:1313/interfaces/java/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/java/Online
- https://example.org/interfaces/online/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/interfaces/online/
+ http://localhost:1313/interfaces/online/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/online/
+
+
+
+ Python
+ http://localhost:1313/interfaces/python/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/python/
+
+
+
+ Rust
+ http://localhost:1313/interfaces/rust/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/interfaces/rust/
diff --git a/interfaces/java/index.html b/interfaces/java/index.html
index f6411eb..3b0f8d4 100644
--- a/interfaces/java/index.html
+++ b/interfaces/java/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,19 @@
+
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 03095f8..4de8a79 100644
--- a/interfaces/java/index.xml
+++ b/interfaces/java/index.xml
@@ -2,18 +2,25 @@
Java on Formal Methods Tools
- https://example.org/interfaces/java/
+ http://localhost:1313/interfaces/java/
Recent content in Java on Formal Methods ToolsHugoen-us
- Fri, 02 Feb 2024 04:14:54 -0800
-
+ 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>
+ Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 e377498..643ce0d 100644
--- a/interfaces/online/index.html
+++ b/interfaces/online/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -83,7 +83,8 @@
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 a18cbd4..f16678f 100644
--- a/interfaces/online/index.xml
+++ b/interfaces/online/index.xml
@@ -2,18 +2,18 @@
Online on Formal Methods Tools
- https://example.org/interfaces/online/
+ http://localhost:1313/interfaces/online/
Recent content in Online on Formal Methods ToolsHugoen-us
- Fri, 02 Feb 2024 04:14:54 -0800
-
+ Sat, 07 Jun 2025 00:00:00 +0000
+ Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 6be7c53..d941d29 100644
--- a/interfaces/python/index.html
+++ b/interfaces/python/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,18 @@
+
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 …
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the …
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 897b0b6..e4afa05 100644
--- a/interfaces/python/index.xml
+++ b/interfaces/python/index.xml
@@ -2,25 +2,32 @@
Python on Formal Methods Tools
- https://example.org/interfaces/python/
+ http://localhost:1313/interfaces/python/
Recent content in Python on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 d5ff788..8883a97 100644
--- a/interfaces/rust/index.html
+++ b/interfaces/rust/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -83,7 +83,7 @@
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 …
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the …
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 90690eb..bd0284b 100644
--- a/interfaces/rust/index.xml
+++ b/interfaces/rust/index.xml
@@ -2,25 +2,25 @@
Rust on Formal Methods Tools
- https://example.org/interfaces/rust/
+ http://localhost:1313/interfaces/rust/
Recent content in Rust on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 858efae..ad1f6a4 100644
--- a/license/index.html
+++ b/license/index.html
@@ -1,6 +1,6 @@
-
+
@@ -16,16 +16,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
diff --git a/licenses/all-rights-reserved/index.html b/licenses/all-rights-reserved/index.html
new file mode 100644
index 0000000..73db33f
--- /dev/null
+++ b/licenses/all-rights-reserved/index.html
@@ -0,0 +1,103 @@
+
+
+
+
+
+
+
+
+All Rights Reserved | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
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 …
+
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 3af4ede..c814b17 100644
--- a/licenses/bsd/index.xml
+++ b/licenses/bsd/index.xml
@@ -2,17 +2,17 @@
BSD on Formal Methods Tools
- https://example.org/licenses/bsd/
+ http://localhost:1313/licenses/bsd/
Recent content in BSD on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/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.html b/licenses/gpl3/index.html
new file mode 100644
index 0000000..a01414b
--- /dev/null
+++ b/licenses/gpl3/index.html
@@ -0,0 +1,95 @@
+
+
+
+
+
+
+
+
+GPL3 | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
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 …
+
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 da24534..2d344f5 100644
--- a/licenses/gplv3/index.xml
+++ b/licenses/gplv3/index.xml
@@ -2,18 +2,32 @@
GPLv3 on Formal Methods Tools
- https://example.org/licenses/gplv3/
+ http://localhost:1313/licenses/gplv3/
Recent content in GPLv3 on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+
+
+ ParaFROST
+ http://localhost:1313/tools/parafrost/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+ Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/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 9100f71..2f4df9f 100644
--- a/licenses/index.html
+++ b/licenses/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -106,6 +106,24 @@
+
+ LGPLv2
+
+
+
+
+
+
+
+
+
+
+
+
Licenses on Formal Methods Tools
- https://example.org/licenses/
+ http://localhost:1313/licenses/
Recent content in Licenses on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+ BSD
- https://example.org/licenses/bsd/
+ http://localhost:1313/licenses/bsd/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/licenses/bsd/
+ http://localhost:1313/licenses/bsd/GPLv3
- https://example.org/licenses/gplv3/
+ http://localhost:1313/licenses/gplv3/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/licenses/gplv3/
+ http://localhost:1313/licenses/gplv3/
+
+
+
+ LGPLv2
+ http://localhost:1313/licenses/lgplv2/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/licenses/lgplv2/MIT
- https://example.org/licenses/mit/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/licenses/mit/
+ http://localhost:1313/licenses/mit/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/licenses/mit/
diff --git a/licenses/lgplv2/index.html b/licenses/lgplv2/index.html
new file mode 100644
index 0000000..b5b629c
--- /dev/null
+++ b/licenses/lgplv2/index.html
@@ -0,0 +1,104 @@
+
+
+
+
+
+
+
+
+LGPLv2 | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 cab9ecf..e02dc89 100644
--- a/licenses/mit/index.xml
+++ b/licenses/mit/index.xml
@@ -2,18 +2,32 @@
MIT on Formal Methods Tools
- https://example.org/licenses/mit/
+ http://localhost:1313/licenses/mit/
Recent content in MIT on Formal Methods ToolsHugoen-us
- Fri, 02 Feb 2024 04:14:54 -0800
-
+ Sat, 07 Jun 2025 00:00:00 +0000
+
+
+ SMT-RAT
+ http://localhost:1313/tools/smt-rat/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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 05f34ad..1b8aab1 100644
--- a/maintenance/actively-maintained/index.html
+++ b/maintenance/actively-maintained/index.html
@@ -1,6 +1,6 @@
-
+
@@ -14,16 +14,16 @@
-
+
-
+
-
-
-
-
+
+
+
+
-
+
@@ -81,9 +81,36 @@
+
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 …
+
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
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 …
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the …
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and …
+
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 a8496f0..678ffd4 100644
--- a/maintenance/actively-maintained/index.xml
+++ b/maintenance/actively-maintained/index.xml
@@ -2,32 +2,53 @@
Actively Maintained on Formal Methods Tools
- https://example.org/maintenance/actively-maintained/
+ http://localhost:1313/maintenance/actively-maintained/
Recent content in Actively Maintained on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+
+
+ SMT-RAT
+ http://localhost:1313/tools/smt-rat/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.</p>Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & 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.html b/maintenance/archived/index.html
new file mode 100644
index 0000000..b3a5c14
--- /dev/null
+++ b/maintenance/archived/index.html
@@ -0,0 +1,104 @@
+
+
+
+
+
+
+
+
+Archived | Formal Methods 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.
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page.
+Colors are generated by hashing each term’s name and converting it to RGB color values.
@@ -227,6 +1603,23 @@
+
+
+
+
+
+
+
+
+
+ SAT Solver
+
+
+
@@ -359,6 +1752,23 @@
+
+
+
+
+
+
+
+
+
+ SAT Solver
+
+
+
diff --git a/tools/index.xml b/tools/index.xml
index b98c1ba..35ed269 100644
--- a/tools/index.xml
+++ b/tools/index.xml
@@ -2,32 +2,109 @@
All Tools on Formal Methods Tools
- https://example.org/tools/
+ http://localhost:1313/tools/
Recent content in All Tools on Formal Methods ToolsHugoen-usSat, 07 Jun 2025 00:00:00 +0000
-
+
+
+ Glucose
+ http://localhost:1313/tools/glucose/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/glucose/
+ <p>Glucose is a SAT solver.</p>
+
+
+ Lingeling
+ http://localhost:1313/tools/lingeling/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/lingeling/
+ <p>Lingeling is a SAT solver.</p>
+
+
+ MathSAT
+ http://localhost:1313/tools/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(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">] </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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ ParaFROST
+ http://localhost:1313/tools/parafrost/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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(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/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/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/
+ 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>
+
+
+ STP
+ http://localhost:1313/tools/stp/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/stp/
+ <p>STP is a constraint solver for quantifier-free bitvectors.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://stp.readthedocs.io/en/latest/#c-library-usage">stp C API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://stp.readthedocs.io/en/latest/#python-usage">stp PyPI package</a></li>
</ul>
+ veriT
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/verit/
+ http://localhost:1313/tools/verit/<p>veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal verification, automated reasoning, and related research areas. veriT accepts input in SMT-LIB2 and DIMACS formats and provides a command-line interface for ease of integration into verification workflows. The solver is actively maintained and distributed under the BSD license, making it suitable for both academic and industrial applications.</p>Yices 2
- https://example.org/tools/yices/
+ http://localhost:1313/tools/yices/
Sat, 07 Jun 2025 00:00:00 +0000
- https://example.org/tools/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>Yices is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/yices/
+ <p>Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>General API:</strong> <a href="https://yices.csl.sri.com/doc/index.html">Yices API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/yices/">yices2 PyPI package</a></li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/yices2">yices2 crate on crates.io</a></li>
</ul>Z3
- https://example.org/tools/z3/
- Fri, 02 Feb 2024 04:14:54 -0800
- https://example.org/tools/z3/
- <p>Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>Z3 is available through several interfaces, making it a convenient option to build into a project.</p>
+ http://localhost:1313/tools/z3/
+ Sat, 07 Jun 2025 00:00:00 +0000
+ http://localhost:1313/tools/z3/
+ <p>Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.</p>
<h2 id="apis-and-bindings">APIs and Bindings</h2>
<p>This tool is available through the following interfaces:</p>
<ul>
<li><strong>C API:</strong> <a href="https://z3prover.github.io/api/html/group__capi.html">Z3 C API Reference</a></li>
<li><strong>C++ API:</strong> <a href="https://z3prover.github.io/api/html/namespacez3.html">Z3 C++ Namespace Reference</a></li>
<li><strong>.NET API:</strong> <a href="https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html">Z3 .NET Namespace Reference</a></li>
<li><strong>Java API:</strong> <a href="https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html">Z3 Java API Reference</a></li>
<li><strong>Python bindings:</strong> <a href="https://pypi.org/project/z3-solver/">z3-solver PyPI package</a> (<a href="https://z3prover.github.io/api/html/z3.html">Documentation</a>)</li>
<li><strong>Rust bindings:</strong> <a href="https://crates.io/crates/z3">z3 crate on crates.io</a></li>
</ul>
diff --git a/tools/lingeling-copy/index.html b/tools/lingeling-copy/index.html
new file mode 100644
index 0000000..290f4cd
--- /dev/null
+++ b/tools/lingeling-copy/index.html
@@ -0,0 +1,300 @@
+
+
+
+
+
+
+
+
+Lingeling | Formal Methods Tools
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine for formal verification. OpenSMT is built on top of MiniSAT.
OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine for formal verification. OpenSMT is built on top of MiniSAT.
ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel.
+
APIs and Bindings
+
This tool is available through the following interfaces:
+ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
+
+
+ (2015)
+
+
+ by Corzilius, Florian et. al.
+ | Appears in SAT 2015
+ (360-368)
+
+
+ | Published by Springer
+ | 10.1007/978-3-319-24318-4_26
+
+
+ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
+
+
+ (2015)
+
+
+ by Corzilius, Florian et. al.
+ | Appears in SAT 2015
+ (360-368)
+
+
+ | Published by Springer
+ | 10.1007/978-3-319-24318-4_26
+
+
+ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
+
+
+ (2015)
+
+
+ by Corzilius, Florian et. al.
+ | Appears in SAT 2015
+ (360-368)
+
+
+ | Published by Springer
+ | 10.1007/978-3-319-24318-4_26
+
+
+ Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality
+
+
+ (2021)
+
+
+ by Henkel, Elisabeth et. al.
+ | Appears in SMT 2021
+
+
+
+
+ | https://ceur-ws.org/Vol-2908/short12.pdf
+
+ Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality
+
+
+ (2021)
+
+
+ by Henkel, Elisabeth et. al.
+ | Appears in SMT 2021
+
+
+
+
+ | https://ceur-ws.org/Vol-2908/short12.pdf
+
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.
+
+
+
+
+
+
+
Publications
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
+
+
+ (2021)
+
+
+ by Schurr, Hans-Jörg et. al.
+ | Appears in CADE 2021
+
+
+
+ | Published by Springer
+ | 10.1007/978-3-030-79876-5_26
+
+
Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories. It supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for research and industrial applications in software and hardware verification.
APIs and Bindings
-
Yices is available through several interfaces, making it a convenient option to build into a project.
+
This tool is available through the following interfaces:
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages.
-Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.
+
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
APIs and Bindings
-
Z3 is available through several interfaces, making it a convenient option to build into a project.
+
This tool is available through the following interfaces:
@@ -488,6 +508,34 @@ Z3 is open source under the MIT license and is actively maintained, making it a
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Z3: An Efficient SMT Solver
@@ -496,7 +544,7 @@ Z3 is open source under the MIT license and is actively maintained, making it a
by de Moura, Leonardo et. al.
- | Appears in TACAS
+ | Appears in TACAS 2008
@@ -511,11 +559,19 @@ Z3 is open source under the MIT license and is actively maintained, making it a