Counterexample Guided Inductive Synthesis Modulo Theories
- Submitting institution
-
University of Edinburgh
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 156000547
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-319-96145-3_15
- Title of conference / published proceedings
- Computer Aided Verification (CAV 2018) Part I
- First page
- 270
- Volume
- 10981
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- July
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
4
- Research group(s)
-
C - Foundations of Computation
- Citation count
- 3
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Counterexample-guided synthesis is a booming area of research, and the CEGIS algorithm is the most prominent instance. This paper, published at CAV, has established a thread of work around generalising communication between the synthesiser and the verifier in CEGIS. Rather than simply rejecting the hypothesis, the verifier replies with qualified feedback. The synthesis engine then prunes a (potentially infinite) set of invalid candidates. The paper also investigates the idea of synthesising solution templates, instead of singleton solutions, which can be completed by first-order solvers. The algorithm proposed has been adopted by CVC4, a leading solver developed at Stanford.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -