English

SyGuS Techniques in the Core of an SMT Solver

Logic in Computer Science 2017-11-30 v1
Authors: Andrew Reynolds , Cesare Tinelli
View on arXiv ↗ PDF ↗ DOI ↗

Abstract

We give an overview of recent techniques for implementing syntax-guided synthesis (SyGuS) algorithms in the core of Satisfiability Modulo Theories (SMT) solvers. We define several classes of synthesis conjectures and corresponding techniques that can be used when dealing with each class of conjecture.

Keywords

syntax-guided synthesis smt solvers synthesis conjectures verification

Cite

@article{arxiv.1711.10641,
  title  = {SyGuS Techniques in the Core of an SMT Solver},
  author = {Andrew Reynolds and Cesare Tinelli},
  journal= {arXiv preprint arXiv:1711.10641},
  year   = {2017}
}

Comments

In Proceedings SYNT 2017, arXiv:1711.10224

Related papers

View all related →
Logic in Computer Science · Computer Science
Approaches for Synthesis Conjectures in an SMT Solver
Andrew Reynolds
2015-10-12
Programming Languages · Computer Science
The SyGuS Language Standard Version 2.1
Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman, Andrew Reynolds +1
2023-12-12
Software Engineering · Computer Science
SyGuS-Comp 2016: Results and Analysis
Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama
2016-11-24
Software Engineering · Computer Science
SyGuS-Comp 2017: Results and Analysis
Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama
2017-12-01
Programming Languages · Computer Science
Results and Analysis of SyGuS-Comp'15
Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama
2016-02-04
Programming Languages · Computer Science
SyGuS-Comp 2018: Results and Analysis
Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh +1
2019-04-16
Logic in Computer Science · Computer Science
What's Decidable about Syntax-Guided Synthesis?
Benjamin Caulfield, Markus N. Rabe, Sanjit A. Seshia, Stavros Tripakis
2016-11-02
Programming Languages · Computer Science
Language to Specify Syntax-Guided Synthesis Problems
Mukund Raghothaman, Abhishek Udupa
2016-10-25
Programming Languages · Computer Science
Overfitting in Synthesis: Theory and Practice (Extended Version)
Saswat Padhi, Todd Millstein, Aditya Nori, Rahul Sharma
2019-06-11
Programming Languages · Computer Science
Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni, Thomas Reps
2020-11-12
Programming Languages · Computer Science
The SemGuS Toolkit
Keith J. C. Johnson, Andrew Reynolds, Thomas Reps, Loris D'Antoni
2024-06-05
Logic in Computer Science · Computer Science
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
Fadil Kallat, Tristan Schäfer, Anna Vasileva
2019-08-27
Artificial Intelligence · Computer Science
Probably Approximately Correct Explanations of Machine Learning Models via Syntax-Guided Synthesis
Daniel Neider, Bishwamittra Ghosh
2020-09-21
Programming Languages · Computer Science
Verifying Solutions to Semantics-Guided Synthesis Problems
Charlie Murphy, Keith Johnson, Thomas Reps, Loris D'Antoni
2025-04-08
Programming Languages · Computer Science
Programming-By-Example by Programming-By-Example: Synthesis of Looping Programs
Shmuel Berman, Mark Santolucito
2021-08-20
Logic in Computer Science · Computer Science
Satisfiability and Synthesis Modulo Oracles
Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
2021-07-29
Logic in Computer Science · Computer Science
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli +1
2015-06-24
Logic in Computer Science · Computer Science
SynRG: Syntax Guided Synthesis of Expressions with Alternating Quantifiers
Elizabeth Polgreen, Sanjit A. Seshia
2020-10-13
Systems and Control · Computer Science
A Counter-Example Guided Framework for Robust Synthesis of Switched Systems Using Control Certificates
Hadi Ravanbakhsh, Sriram Sankaranarayanan
2016-02-11
Artificial Intelligence · Computer Science
Guiding Enumerative Program Synthesis with Large Language Models
Yixuan Li, Julian Parsert, Elizabeth Polgreen
2024-05-28
Machine Learning · Computer Science
Grammar Filtering For Syntax-Guided Synthesis
Kairo Morton, William Hallahan, Elven Shum, Ruzica Piskac +1
2020-02-10
Programming Languages · Computer Science
Proving Unrealizability for Syntax-Guided Synthesis
Qinheping Hu, Jason Breck, John Cyphert, Loris D'Antoni +1
2019-07-25
Artificial Intelligence · Computer Science
Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis
Julian Parsert, Elizabeth Polgreen
2024-01-08
Programming Languages · Computer Science
Using SyGuS to Synthesize Reactive Motion Plans
Sarah Chasins, Julie L. Newcomb
2016-11-24
Software Engineering · Computer Science
Genetic Algorithms for Searching a Matrix of Metagrammars for Synthesis
Yixuan Li, Federico Mora, Elizabeth Polgreen, Sanjit A. Seshia
2023-06-06