BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Programming Constraint Services with Z3
DTSTART:20170308T140000
DTEND:20170308T150000
DTSTAMP:20260407T231014Z
UID:9fe2733baaf798fa72030fde14ced0151c4854f8cb8f7b5ebe2db24e
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Nikolaj Bjorner\n\nAbstract\nMany program verification\, an
 alysis\, testing and synthesis queries reduce to solving satisfiability of
  logical formulas. Yet\, there are several applications where satisfiabili
 ty\, and optionally a model or a proof\, is insufficient. Examples of usef
 ul additional information include interpolants\, models that satisfy optim
 ality criteria\, generating strategies for solving quantified formulas\, e
 numerating and counting solutions. We will cover some of the newer feature
 s in Z3 that expose constraint services. For applications in product confi
 guration\, Z3 includes specialized solvers for finding backbones under ass
 umptions\, for solving quantified formulas Z3 contains elements of partial
  quantifier elimination methods based on models\, and for solving optimiza
 tion modulo SMT\, Z3 contains dedicated MaxSMT.\n\nBio\nNikolaj Bjorner is
  a Principal Researcher at Microsoft Research\, Redmond\, working in the a
 rea of Automated Theorem Proving and Software Engineering. His current mai
 n line of work with Leonardo de Moura  and Christoph Wintersteiger is aro
 und the state-of-the art theorem prover Z3\, which is used as a foundation
  of several software engineering tools. Z3 received the 2015 ACM SIGPLAN S
 oftware System award and most influential tool paper in the first 20 years
  of TACAS in 2014. Previously\, he developed the DFSR\, Distributed File S
 ystem - Replication\, and Remote Differential Compression protocols\, RDC\
 , part of Windows Server since 2005 and before that worked on distributed 
 file sharing systems at a startup\, and program synthesis and transformati
 on systems at the Kestrel Institute. He received his Master’s and Ph.D. 
 degrees in computer science from Stanford University\, and spent the first
  few years of university at DTU and DIKU.\n\nMore information
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR