Go to
Viktor Kuncak
Professor
Laboratory for Automated Reasoning and Analysis
School of Computer and Communication Sciences
EPFL, Switzerland
Synthesis Inside Satisfiability Modulo Theory Solvers
Thursday, 10 December 2015 at 16:40 in room BC 420
Abstract:
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from un- satisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifier instantiation that we use to make finding such proofs practically feasible. A particularly important class of specifications are single-invocation properties, for which we present a dedicated algorithm. To support syntax restrictions on generated solutions, our approach can transform a solution found without restrictions into the desired syntactic form. As an alternative, we show how to use evaluation function axioms to embed syntactic restrictions into constraints over algebraic datatypes, and then use an algebraic datatype decision procedure to drive synthesis. Our experimental eval- uation on syntax-guided synthesis benchmarks shows that our implementation in the CVC4 SMT solver is competitive with state-of-the-art tools for synthesis.
About the speaker:
Viktor Kuncak is an associate professor at the EPFL School of Computer and Communication Sciences, where he leads the Laboratory for Automated Reasoning and Analysis (http://lara.epfl.ch). He works in formal methods with emphasis on algorithms and tools, such as Leon (http://leon.epfl.ch). He received a PhD degree from the Massachusetts Institute of Technology (MIT) in 2007. He was a program co-chair of FMCAD 2014 and VMCAI 2012, and led an international COST Action to establish standardized formats for verification and synthesis (Rich Model Toolkit). His invited talks include those at LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. He received an ACM SIGSOFT distinguished paper award for work on automated testing. His work on software synthesis procedures was published in the Communications of the ACM as a Research Highlight article. His recent work on Implicit Programming, funded by a European Research Council (ERC) grant, aims to bridge the gap between human goals and their computational realizations.
Secondary navigation
- EPFL Workshop on Logic Synthesis and Emerging Technologies
- Luca Amaru
- Luca Benini
- Giovanni De Micheli
- Srini Devadas
- Antun Domic
- Rolf Drechsler
- Pierre-Emmanuel Gaillardon
- Jie-Hong Roland Jiang
- Akash Kumar
- Shahar Kvatinsky
- Yusuf Leblebici
- Shin-ichi Minato
- Alan Mishchenko
- Vijaykrishnan Narayanan
- Ian O'Connor
- Andre Inacio Reis
- Martin Roetteler
- Julien Ryckaert
- Mathias Soeken
- Christof Teuscher
- Zhiru Zhang
- Symposium on Emerging Trends in Computing
- Layout synthesis: A golden DA topic
- EPFL Workshop on Logic Synthesis & Verification
- Luca Amaru
- Luca Benini
- Robert Brayton
- Maciej Ciesielski
- Valentina Ciriani
- Jovanka Ciric-Vujkovic
- Jason Cong
- Jordi Cortadella
- Giovanni De Micheli
- Antun Domic
- Rolf Drechsler
- Henri Fraisse
- Paolo Ienne
- Viktor Kuncak
- Enrico Macii
- Igor Markov
- Steven M. Nowick
- Tsutomu Sasao
- Alena Simalatsar
- Leon Stok
- Dirk Stroobandt
- Tiziano Villa
- Symposium on Emerging Trends in Electronics
- Raul Camposano
- Anantha Chandrakasan
- Jo De Boeck
- Gerhard Fettweis
- Steve Furber
- Philippe Magarshack
- Takayasu Sakurai
- Alberto Sangiovanni-Vincentelli
- Ken Shepard
- VENUE
- Panel on Circuits in Emerging Nanotechnologies
- Panel on Emerging Methods of Computing
- Panel on The Role of Universities in the Emerging ICT World
- Panel on Design Challenges Ahead
- Panel on Alternative Use of Silicon
- Nano-Bio Technologies for Lab-on-Chip
- Functionality-Enhanced Devices Workshop
- More Moore: Designing Ultra-Complex System-on-Chips
- Design Technologies for a New Era
- Nanotechnology for Health
- Secure Systems Design
- Surface Treatments and Biochip Sensors
- Security/Privacy of IMDs
- Nanosystem Design and Variability
- Past Events Archive
Presentation Slides
On-line Registration
Registration is now closed. We have reached the maximum number of registrants. We thank you for your interest in our workshop!
Venue
All talks will take place at EPFL room BC 420. Please click HERE to go to the interactive EPFL map.