The Varied Forms of Verification with Z3

The Z3 theorem prover is Microsoft’s main engine of logic and it is used in a variety of projects. It is rooted in the need for efficient decision procedures in the area of software verification, and it has since been extended into bordering areas. Emerging applications include verification of probabilistic properties of software and other systems, as well as verification and synthesis of biological systems, both constructed and natural.

In this talk, I will briefly introduce the core concepts involved in verification(-like) problems, and I will demonstrate how theorem provers in general, and Z3 specifically, are employed to solve many of the subproblems that arise. I will then touch upon the satisfiability problem for the theory of floating-point numbers as an example of the design of a tailored decision procedure for a particular theory. The last part of the talk will be spent on various applications of this and other decision procedures to problems that arise in computer science and in computational biology.