Campus Event Calendar
Event Entry
New for: D1, D3, D4, D5
What and Who
SMT@Microsoft
Leonardo de Moura
Microsoft
Virtual Seminar
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 19 October 2009
16:00
60 Minutes
E1 4
019
Saarbrücken
Warning: New Room!
Abstract
Program analysis and verification require decision procedures for satisfiability modulo theories (SMT), that decide the satisfiability, or, dually, the validity, of formulas in decidable fragments of specific theories or combinations thereof. Examples include the quantifier-free fragments of theories of arithmetic, bit-vectors, lists, arrays and records. The challenge is to have decision procedures that are simultaneously sound, complete, expressive and efficient, to handle problems of practical interest without incurring in false negatives or false positives. SMT solvers have proven highly scalable, efficient and suitable for integrating theory reasoning.
The success of SMT for program analysis and verification is largely due to the suitability of supported background theories. In this talk, we describe how SMT solvers, with emphasis on Microsoft's Z3 solver, are used in program analysis and verification. Several concrete applications from program analysis at Microsoft will be presented.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 10/19/2009 08:57 -- Created document.