Yices 2

Quick Links

At a Glance

Developers	SRI International
Domains	Software Verification Hardware Verification Embedded Systems
Formalisms	first-order logic SMT-LIB quantifier logic bit-vectors arrays uninterpreted functions arithmetic
Interactions	CLI C API OCaml API Python Bindings
Languages	SMT-LIB Yices language C OCaml Python
Purposes	Verification Tools Analysis Tools
Systems	Discrete Systems Concurrent Systems
Techniques	Theorem Proving SMT Solving Model Checking

Description

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.

Publications

Yices 2.2 (July 2014) by Dutertre, Bruno | Appears in Computer-Aided Verification (737-744) | Volume 8559 | Published by Springer