|
CS Home
Dept Info/Contacts
People
Research
Events
Courses
Undergrad Programs:
Computer Science
Informatics
Graduate Program
Prospective Students
Faculty Hiring
Employment
Resources
Help Lab Hours
Student Groups
Support the Department: Weeg Professorship
|
|
SMT@Microsoft
Friday, Sep 11, 2009
4:00-5:00pm, S401, John Pappajohn Business Building
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.
|
