Conference proceeding
Extending enumerative function synthesis via SMT-driven classification
2019 Formal Methods in Computer Aided Design (FMCAD), pp.212-220
10/2019
DOI: 10.23919/FMCAD.2019.8894267
Abstract
Many relevant problems in formal methods can be tackled using enumerative syntax-guided synthesis (SyGuS). Algorithms for enumerative SyGuS range from universally applicable techniques based on counterexample-guided inductive synthesis (CEGIS), to more scalable but specialized techniques based on divide and conquer. This paper presents a novel algorithm for enumerative SyGuS, Unif + PI, which reaps the benefits of scalability based on divide and conquer without sacrificing generality. In this algorithm, an instance of an SMT solver is used as both a classifier and an attribute generator. Logical constraints in the form of test cases for the function-to-synthesize and failed classification attempts guide its search for new candidate solutions. We implement our approach as an extension of the CVC4SY solver and evaluate it on standard SyGuS benchmarks from different applications. We show that the new algorithm leads to significant gains in invariant synthesis with respect to state-of-the-art SyGuS solvers, and is competitive with state-of-the-art k-induction based model checking.
Details
- Title: Subtitle
- Extending enumerative function synthesis via SMT-driven classification
- Creators
- Haniel Barbosa - University of IowaAndrew Reynolds - University of IowaDaniel Larraz - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- 2019 Formal Methods in Computer Aided Design (FMCAD), pp.212-220
- DOI
- 10.23919/FMCAD.2019.8894267
- eISSN
- 2642-732X
- Publisher
- FMCAD Inc
- Language
- English
- Date published
- 10/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259476202771
Metrics
35 Record Views