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.
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
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.