BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Model-Based Reasoning About Quantified Formulas in SMT
DTSTART:20130918T140000
DTEND:20130918T150000
DTSTAMP:20260406T225957Z
UID:3c69618950bd7028c07891a389983d0129a8c2782b631f36831f8c3a
CATEGORIES:Conferences - Seminars
DESCRIPTION:Andrew Reynolds\nSatisfiability Modulo Theories (SMT) solvers 
 have emerged as powerful tools in formal methods applications in recent ye
 ars\, due in part to advances in decision procedures for ground theories f
 or arithmetic\, arrays\, bit-vectors and recursive datatypes.  An ongoing
  challenge in the SMT community has been how to handle the presence of uni
 versally quantified formulas.  Typically\, when such formulas are present
 \, a solver will either answer "unsatisfiable" if the solver is able to fi
 nd a proof\, or otherwise will answer "unknown" after some predetermined a
 mount of effort.  For many applications\, however\, it is often critical 
 to know when such formulas are guaranteed to be satisfiable\, and moreover
  to have a model that demonstrates the satisfiability.  For instance\, in
  verification applications\, a model may correspond to a concrete countere
 xample for safety property in question.\nThis talk examines various model-
 based approaches for reasoning about quantified formulas in SMT.  One app
 roach\, finite model finding\, can establish the satisfiability of a quant
 ified formula whose domain is finite by exhaustively testing all of its gr
 ound instances.  While this may not be practical for quantified formulas 
 with large domain sizes\, various techniques can minimize domain sizes and
  identify when sets of instances are not relevant.  Similar approaches ma
 y be applied to further domains and applications\, including the case of q
 uantification over integer variables where finite bounds can be inferred.
   Experimental results are given for an implementation of a finite model 
 finding capability in the SMT solver CVC4.
LOCATION:INR331 http://plan.epfl.ch/?room=INR%20331
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR