Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Synthesis from within: implementing automated synthesis inside an SMT solver
Speaker:Cesare Tinelli
coming from:University of Iowa
Speakers Bio:Cesare Tinelli received a Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign in 1999 and is a F. Wendell Miller Professor at the University of Iowa. His main research interests are in automated reasoning and their applications in formal methods. He has done seminal work in Satisfiability Modulo Theories (SMT), a subfield of automated reasoning he helped establish through his research and service activities. His research has appeared in more than 80 refereed publications and has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, NSF, and ONR) and corporations (Amazon, Intel, General Electric, Rockwell Collins, and United Technologies). He leads the development of the Kind 2 model checker and co-leads the development of the widely used and award winning CVC4 SMT solver. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He is an associate editor of the Journal of Automated Reasoning and a co-founder of the SMT workshop series and the Midwest Verification Day series. He has served in the program committee of more than 70 automated reasoning and formal methods conferences and workshops, as well as the steering committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was the PC chair of FroCoS’11 and a PC co-chair of TACAS’15. He has given invited talks or tutorials at CADE, CAV, ETAPS, FroCoS, HVC, NSV, TABLEAUX, VSTTE, and WoLLIC.
Event Type:SWS Colloquium
Visibility:D1, D2, D3, INET, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Monday, 16 September 2019
Duration:60 Minutes
Recent research in automated software synthesis from specifications or observations has leveraged the power of SMT solvers in order to explore the space of synthesis conjectures efficiently. In most of this work, synthesis techniques are built around a backend SMT solver which is used as a black-box reasoning engine. In this talk, I will describe a successful multiyear research effort by the developers of the SMT solver CVC4 that instead incorporates synthesis capabilities directly within the solver, and the discuss the advances in performance and scope made possible by this approach.
Name(s):Mouna Litz
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:E1 5To Room:029
Meeting ID:SWS Space 2 (6312)
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Mouna Litz, 09/12/2019 01:19 PM
  • Mouna Litz, 09/12/2019 01:18 PM -- Created document.