BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Monday Seminars : "The Satisfiability Modulo Theories solver Z3
  and its Applications"
DTSTART:20111107T141500
DTSTAMP:20260406T185156Z
UID:1504eaa2db16f93af9ea539811c6d35341ea25ba8f45eb8532587747
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr. Nikolaj Bjorner - Microsoft Research\nAbstract Modern soft
 ware analysis and model-based tools are increasingly complex and multi-fac
 eted software systems. However\, at their core is invariably a component u
 sing logical formulas for describing states and transformations between sy
 stem 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. S
 MT solvers have been the focus of increased recent attention thanks to tec
 hnological advances and an increasing number of applications. The Z3 SMT s
 olver is used in several program analysis\, testing and design tools at Mi
 crosoft Research\, in the Windows 7 static driver verifier\, and in many t
 ools 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 overvie
 w 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 solve
 r 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 imp
 lemented the core of the distributed file replication system\, DFS-R\, and
  the content dependent chunking algorithms in the remote differential comp
 ression protocol RDC. To contact Dr. Nikolaj Bjorner\, please email Prof. 
 Viktor Kuncak (viktor.kuncak@epfl.ch)
LOCATION:INR 219
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR