BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:An Efficient Solver for string and regular expression constraints 
  - Cesare Tinelli\, University of Iowa
DTSTART:20150409T090000Z
DTEND:20150409T100000Z
UID:TALK58406@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:An increasing number of applications in verification and secur
 ity rely on or could benefit from automatic solvers that can check the sat
 isfiability of constraints over a rich set of data types that includes cha
 racter strings. Until recently\, available string solvers were standalone 
 tools that could reason only about (some fragment) of the theory of string
 s and regular expressions\, sometimes with strong restrictions on the expr
 essiveness of their input language. These solvers were based on reductions
  to satisfiability problems over other data types\, such as bit vectors\, 
 or to automata decision problems. In this talk\, we present a set of algeb
 raic techniques for solving constraints over the theory of unbounded strin
 gs natively\, without a reduction to other problems. These techniques can 
 be used to integrate string reasoning into general solvers for satisfiabil
 ity modulo theories (SMT). We have implemented them in our SMT solver CVC4
  to expand its large set of built-in theories to a theory of strings with 
 concatenation\, length\, and membership in regular languages. Our initial 
 experimental results show that\, in addition\, over pure string problems\,
  CVC4 is highly competitive with specialized string solvers with a compara
 ble input language. 
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR