Computer Science Colloquium

Leonardo de Moura, Nikolaj Bjorner
Microsoft Research

Satisfiability Modulo Theories @ Microsoft

Fri 04.04.2008, 10:15, 60 minutes
HS 3

Abstract

This talk presents recent and ongoing advances in software verification applications using, and the development of, automated verification technologies at Microsoft Research. A number of in-house projects rely on SMT solvers: The Static Driver Verifier, SDV, is shipped in Windows. It uses decision procedures and symbolic model checking to statically find bugs in device drivers. The Pex and related projects use automated decision procedures to analyze the results of runs for generating unit tests by using model finding capabilities of the decision procedures. Other projects using similar capabilities of the solvers are whitebox fuzz testing, predicate abstraction, and internet worm prevention. The Spec# project comprises of an object oriented programming language extending C# with contracts together with an verification oriented intermediary format, called Boogie, used for extracting verification conditions. A new ambitious project in the context of Boogie, but applied to production C-code, is a comprehensive functional verification of the Hyper-V virtualization core. The talk will cover these applications and the unique opportunities they provide for enhancing validation during the software development process. Several of the presented projects use as core technology a Satisfiability Modulo Theories solver, Z3, developed by the speakers. The above application will be presented with an emphasis on how they exercise and have shaped the solver. Z3 is available at: http://research.microsoft.com/projects/z3

Invited by Prof. Dr. Armin Biere

---

The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).

List of all talks