1.6 KiB
+++ date = 2024-02-02T04:14:54-08:00 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'] 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" } ] 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.
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.