Encoding Custom Theories in Z3

Introduction

Automated program verification has made significant progress in recent years, partially due to advancements made in the underlying theorem provers which are used to check if all necessary assertions hold. One such theorem prover is the freely available SMT solver Z3 developed by Microsoft, which is used as an important building block in many verification and testing tools.
Being an SMT solver, Z3 has built-in support for various theories such as booleans and integers, but also enables developers to add support for custom theories such as lists and sets.

The performance of SMT solvers is usually affected by three aspects: the problem solving routines (subsolvers), e.g., for a given boolean problem, the heuristics guiding these subsolvers, and the problem encoding chosen by the user. From a user's perspective the latter is especially important, because it can have a significant impact on the performance of the solver, and because it is the aspect over which the user has the best control.

Goals

A new major version of Z3 has been released recently, which contains revised (as well as new) subsolvers, and additional possibilities for users to encode their own theories. The goals of this Research in Computer Science project are to

Get an overview of the latest changes and features, especially about support for abstract data types
Identify different possibilities of encoding custom theories arising from our work on automated program verification, e.g., lists and sets, and access permissions, which are used to control write effects in concurrent systems
Prototypically encode these theories in different ways
Evaluate different encodings of the same theory

Opportunities

Work with state-of-the-art verification tools
Gain experience with the formal encoding of fundamental data structures
Influence the future development of our open source tools
Interact with our researchers and PhD students and attend meetings for other ongoing research projects

Recommended background

Interest in formal methods

Contact

Malte Schwerhoff