Microsoft Research Z3 Theorem Prover

  • Microsoft Research Z3 Theorem Prover
 

Microsoft Research Z3 Theorem Prover

USD$14,950.00

A high-performance theorem prover that includes custom solvers for data-type theories common in program testing, verification, synthesis and analysis.

Quantity:

A high-performance theorem prover that includes custom solvers for data-type theories common in program testing, verification, synthesis and analysis.

 

 

Microsoft Research Z3 is a high-performance theorem prover that includes many efficient custom solvers for data-type theories that are common in program testing, verification, synthesis, and analysis.

Z3 integrates efficient constraint solving technologies for propositional satisfiability, free functions, linear arithmetic over the reals and integers, bit-vectors, algebraic data types, and applicative arrays. It can be used for checking satisfiability of logical formulas with quantifiers, as well by leveraging quantifier instantiation procedures, saturation, and quantifier-elimination procedures for reals, integers, and algebraic data types.

Besides supporting a rich base of theories, Z3 is also highly customizable with an extensive API and support for custom theories.

  • High-performance theorem prover
  • Checks satisfiability of logical formulas with quantifiers
  • Includes support for custom theories
  • Integrates efficient constraint solving technologies
  • Highly customizable with an extensive API

Requirements

Required Processor
2 GHz or faster
Required Operating System
Windows 7, Vista, or XP SP3
Required Memory
1GB