BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Building Better SMT Solvers using Syntax-Guided Synthesis
DTSTART:20190523T114500
DTEND:20190523T124500
DTSTAMP:20260501T144436Z
UID:8b689700af5a345c0e438d3c675f86674b0362a13c9ea8ac6d0cbccf
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Andrew Reynolds\n\nAbstract\nSatisfiability Modulo Theories
  (SMT) solvers have gained widespread popularity as reasoning engines in n
 umerous formal methods applications\, including in syntax-guided synthesis
  (SyGuS) applications. Previous work has also shown that SMT solvers\, not
 ably CVC4\, can act as efficient stand-alone synthesis solvers.\nIn this t
 alk\, we focus on a emerging class of applications for syntax-guided synth
 esis\, namely\, the use of a SyGuS solver to (partially) automate further 
 development and improvements to the solver itself. We describe several rec
 ent features in the SMT solver CVC4 that follow this paradigm. These inclu
 de syntax-guided enumeration of rewrite rules\, selection of test inputs\,
  and discovery of solved forms for quantified constraints. For the latter\
 , we describe how syntax-guided synthesis recently played a pivotal role i
 n the development of a new algorithm for quantified bit-vector constraints
  based on invertibility conditions\, and how this technique can be extende
 d for similar algorithms that target quantified constraints in other theor
 ies\, including the theory of floating points.\n\nBio\nAndrew Reynolds is 
 a research scientist at the University of Iowa\, and one of the lead devel
 opers of the Satisfiability Modulo Theories (SMT) solver CVC4. His researc
 h spans various aspects of SMT solving\, including approaches for (syntax-
 guided) synthesis conjectures\, unbounded strings and regular expressions\
 , and first-order theorem proving. His work in CVC4 has entered numerous c
 ompetitions and has received awards spanning several automated reasoning c
 ommunities\, including SMT\, automated theorem proving\, and syntax-guided
  synthesis.\n\nMore information\n 
LOCATION:INR 331 https://plan.epfl.ch/?room=INR331
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR