fmtools/content
1
0
Fork 0
Code Issues 20 Pull Requests Actions Packages Releases Wiki Activity

add solvers

Browse Source
This commit is contained in:
Landon Taylor
2025-06-09 11:45:37 -06:00
parent 388d5fb8f9
commit a454011c40
9 changed files with 146 additions and 47 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
tools/verit.md Normal file
View File

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

40
tools/yices.md
View File

@@ -1,29 +1,31 @@
+++
date = 2024-02-02T04:14:54-08:00
date = 2025-06-07
draft = false
title = 'Yices 2'
purposes = ['Verification Tools', 'Analysis Tools']
techniques = ['Theorem Proving', 'SMT Solving', 'Model Checking']
domains = ['Software Verification', 'Hardware Verification', 'Embedded Systems']
languages = ['SMT-LIB', 'Yices language', 'C', 'OCaml', 'Python']
systems = ['Discrete Systems', 'Concurrent Systems']
interactions = ['CLI', 'C API', 'OCaml API', 'Python Bindings']
formalisms = ['first-order logic', 'SMT-LIB', 'quantifier logic', 'bit-vectors', 'arrays', 'uninterpreted functions', 'arithmetic']
developers = ['SRI International']
subtitle = 'SMT Solver'
links = [
{ title = "Homepage", url = "https://yices.csl.sri.com/" },
{ title = "Source Code", url = "https://github.com/SRI-CSL/yices2" },
{ title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
{ title = "Homepage", url = "https://yices.csl.sri.com/", icon = 'fa-solid fa-home'},
{ title = "Source Code", url = "https://github.com/SRI-CSL/yices2", icon = 'fa-brands fa-github' },
# { title = "Documentation", url = "https://yices.csl.sri.com/yices2-documentation.html" }
]
applications = ['SMT Solver']
developers = ['SRI International']
licenses = ['GPLv3']
inputs = ['SMTLIB2', 'Yices 2']
interfaces = ['CLI', 'Python', 'Rust']
maintenance = ['Actively Maintained']
publications = ['Dutertre2014']
+++
Yices is a high-performance SMT solver and theorem prover developed by SRI International. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Yices supports the SMT-LIB standard and its own input language, and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.
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.
### Features
- **SMT Solver:** Supports a wide range of theories and quantifiers.
- **Multi-language APIs:** C, OCaml, Python, and more.
- **Cross-platform:** Available on Windows, Linux, and macOS.
- **Active development:** Open source and maintained by SRI International.
## APIs and Bindings
Yices is available through several interfaces, making it a convenient option to build into a project.
- **General API:** [Yices API Reference](https://yices.csl.sri.com/doc/index.html)
- **Python bindings:** [yices2 PyPI package](https://pypi.org/project/yices/)
- **Rust bindings:** [yices2 crate on crates.io](https://crates.io/crates/yices2)

44
tools/z3.md
View File

@@ -2,31 +2,33 @@
date = 2024-02-02T04:14:54-08:00
draft = false
title = 'Z3'
purposes = ['Verification Tools', 'Analysis Tools']
techniques = ['Theorem Proving', 'SMT Solving', 'Model Checking']
domains = ['Software Verification', 'Hardware Verification', 'Embedded Systems']
languages = ['SMT-LIB', 'Python', 'C++', 'Java', 'C#']
systems = ['Discrete Systems', 'Concurrent Systems']
interactions = ['CLI', 'Python API', 'Rust Bindings', 'playground']
formalisms = ['first-order logic', 'SMT-LIB', 'quantifier logic', 'bit-vectors', 'arrays', 'uninterpreted functions', 'arithmetic']
subtitle = 'Theorem Prover'
links = [
{ title = "Homepage", url = "https://github.com/Z3Prover/z3", icon = 'fa-solid fa-home' },
{ title = "Source Code", url = "https://github.com/Z3Prover/z3", icon = 'fa-brands fa-github' },
{ title = "Playground", url = "https://jfmc.github.io/z3-play/", icon = 'fa-solid fa-gamepad' }
]
applications = ['SMT Solver', 'Theorem Prover']
developers = ['Microsoft Research']
licenses = ['MIT']
links = [
{ title = "Homepage", url = "https://github.com/Z3Prover/z3" },
{ title = "Source Code", url = "https://github.com/Z3Prover/z3" },
{ title = "Discussions", url = "https://github.com/Z3Prover/z3/discussions" },
{ title = "Documentation", url = "https://z3prover.github.io/api/html/" },
{ title = "Playground", url = "https://rise4fun.com/z3" }
]
inputs = ['SMTLIB2', 'DIMACS']
interfaces = ['CLI', 'Python', 'Rust', 'C', 'C++', 'Java', '.NET', 'Online']
maintenance = ['Actively Maintained']
# techniques = ['CDCL']
publications = ['deMoura2008']
+++
Z3 is a high-performance SMT solver and theorem prover developed by Microsoft Research. It is widely used for checking the satisfiability of logical formulas over various theories, including arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 supports the SMT-LIB standard and provides APIs for several programming languages, making it suitable for integration into formal verification, program analysis, and constraint solving tools.
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.
## APIs and Bindings
Z3 is available through several interfaces, making it a convenient option to build into a project.
- **C API:** [Z3 C API Reference](https://z3prover.github.io/api/html/group__capi.html)
- **C++ API:** [Z3 C++ Namespace Reference](https://z3prover.github.io/api/html/namespacez3.html)
- **.NET API:** [Z3 .NET Namespace Reference](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
- **Java API:** [Z3 Java API Reference](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
- **Python bindings:** [z3-solver PyPI package](https://pypi.org/project/z3-solver/) ([Documentation](https://z3prover.github.io/api/html/z3.html))
- **Rust bindings:** [z3 crate on crates.io](https://crates.io/crates/z3)
### Features
- **SMT Solver:** Supports a wide range of theories and quantifiers.
- **Multi-language APIs:** Python, C++, Java, .NET, and more.
- **Cross-platform:** Available on Windows, Linux, and macOS.
- **Active development:** Open source and maintained by Microsoft Research.
- **Web Playground:** Try Z3 online at [Rise4Fun](https://rise4fun.com/z3).