Program
Verification
Book

PV4 ⊧ Z3produces a satisfiability result for a formula

Application domain/field

SMT (Satisfiability Modulo Theories)
SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB v2 format There are bindings for .NET, C, C++, Java, OCaml, Python, Julia and Web Assembly

Expected output

sat, unsat or unknown

Links

https://github.com/Z3Prover/z3

Last commit date: 02 Dec 2022 (default branch)
Last commit date: 03 Dec 2022 (last activity)

Related papers

Z3: An Efficient SMT Solver (TACAS '08)
νZ - An Optimizing SMT Solver (TACAS '15)
See also: https://github.com/Z3Prover/z3/wiki/Publications

Last publication date

April 2015

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.