IC Monday Seminars : "The Satisfiability Modulo Theories solver Z3 and its Applications"
Event details
| Date | 07.11.2011 |
| Hour | 14:15 |
| Speaker | Dr. Nikolaj Bjorner - Microsoft Research |
| Location |
INR 219
|
| Category | Conferences - Seminars |
Abstract Modern software analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using logical formulas for describing states and transformations between system states. In a nutshell, symbolic logic is the calculus of computation. The state-of-the art Satisfiability Modulo Theories (SMT) solver, Z3, developed by Leonardo de Moura and the speaker at Microsoft Research, can be used to check the satisfiability of logical formulas over one or more theories. SMT solvers offer a compelling match for software tools, since several common software constructs map directly into supported theories. SMT solvers have been the focus of increased recent attention thanks to technological advances and an increasing number of applications. The Z3 SMT solver is used in several program analysis, testing and design tools at Microsoft Research, in the Windows 7 static driver verifier, and in many tools outside of Microsoft. It offers a rich interface and set of features and is also the most efficient solver available in most areas exercised by SMT solvers. The talk presents the background of Z3 and offers an overview of some of the many applications. Biography I am a senior researcher in the Research in Software Engineering group at Microsoft Research, Redmond. My main line of work is around the state-of-the-art SMT constraint solver Z3 with Leonardo de Moura. Z3 is used for program verification and test case generation. In a previous lives I wrote STeP, the Stanford Temporal Prover, and I was in the Core File Systems group where I designed and implemented the core of the distributed file replication system, DFS-R, and the content dependent chunking algorithms in the remote differential compression protocol RDC. To contact Dr. Nikolaj Bjorner, please email Prof. Viktor Kuncak ([email protected])
Links
Practical information
- General public
- Free
Contact
- Simone Muller