CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis

Andrew Reynolds; Haniel Barbosa; Andres Notzli; Clark Barrett; Cesare Tinelli

doi:10.1007/978-3-030-25543-5_5

Back

CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis

Conference proceeding

Open access

Peer reviewed

CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis

Andrew Reynolds, Haniel Barbosa, Andres Notzli, Clark Barrett and Cesare Tinelli

COMPUTER AIDED VERIFICATION, CAV 2019, PT II, Vol.11562, pp.74-83

Lecture Notes in Computer Science

01/01/2019

DOI: 10.1007/978-3-030-25543-5_5

Files and links (1)

url

https://doi.org/10.1007/978-3-030-25543-5_5View

Published (Version of record) Open Access

Abstract

We present CVC4SY, a syntax-guided synthesis (SyGuS) solver based on three bounded term enumeration strategies. The first encodes term enumeration as an extension of the quantifier-free theory of algebraic datatypes. The second is based on a highly optimized brute-force algorithm. The third combines elements of the others. Our implementation of the strategies within the satisfiability modulo theories (SMT) solver CVC4 and a heuristic to choose between them leads to significant improvements over state-of-the-art SyGuS solvers.

Computer Science

Technology

Computer Science, Software Engineering

Computer Science, Theory & Methods

Science & Technology

Details

Title: Subtitle: CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
Creators: Andrew Reynolds - University of Iowa
Haniel Barbosa - Univ Iowa, Iowa City, IA USA
Andres Notzli - Stanford University
Clark Barrett - Stanford University
Cesare Tinelli - University of Iowa
Contributors: Isil Dillig (Editor)
Serdar Tasiran (Editor)
Resource Type: Conference proceeding
Publication Details: COMPUTER AIDED VERIFICATION, CAV 2019, PT II, Vol.11562, pp.74-83
Series: Lecture Notes in Computer Science
DOI: 10.1007/978-3-030-25543-5_5
ISSN: 0302-9743
eISSN: 1611-3349
Publisher: Springer Nature
Number of pages: 10
Grant note: 1656926 / National Science Foundation; National Science Foundation (NSF) FA8650-18-2-7854 / Defense Advanced Research Projects Agency; United States Department of Defense; Defense Advanced Research Projects Agency (DARPA)
Language: English
Date published: 01/01/2019
Academic Unit: Computer Science
Record Identifier: 9984411252702771

Metrics

8 Record Views

47 Times Cited - Web of Science