research-article

Can reactive synthesis and syntax-guided synthesis be friends?

Authors:

Bernd Finkbeiner,

Mark SantolucitoAuthors Info & Claims

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 229 - 243

https://doi.org/10.1145/3519939.3523429

Published: 09 June 2022 Publication History

Abstract

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic modulo theories (TSL-MT), a framework that unites the two approaches to synthesize a single program. In our approach, reactive synthesis and SyGuS collaborate in the synthesis process, and generate executable code that implements both reactive and data-level properties.

We present a tool, temos, that combines state-of-the-art methods in reactive synthesis and SyGuS to synthesize programs from TSL-MT specifications. We demonstrate the applicability of our approach over a set of benchmarks, and present a deep case study on synthesizing a music keyboard synthesizer.

References

[1]

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. IEEE.

[2]

Rajeev Alur, Dana Fisman, Saswat Padhi, Andrew Reynolds, Rishabh Singh, and Abhishek Udupa. 2019. The 6th Competition on Syntax-Guided Synthesis. https://sygus.org/comp/2019/results-slides.pdf Accessed: 2019-11-20.

[3]

Sourav Anand and Nadia Polikarpova. 2018. Automatic Synchronization for GPU Kernels. In Formal Methods in Computer Aided Design, FMCAD. IEEE. https://doi.org/10.23919/FMCAD.2018.8602999

[4]

C.P.R. Baaij. 2015. Digital circuit in Cλ aSH: functional specifications and type-directed synthesis. Ph.D. Dissertation. University of Twente. isbn:978-90-365-3803-9 https://doi.org/10.3990/1.9789036538039 eemcs-eprint-23939.

[5]

Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. In Handbook of Model Checking. Springer.

[6]

Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification - 23rd International Conference, CAV (Lecture Notes in Computer Science, Vol. 6806). Springer. https://doi.org/10.1007/978-3-642-22110-1_14

[7]

Roderick Bloem, Swen Jacobs, and Ayrat Khalimov. 2014. Parameterized synthesis case study: AMBA AHB (extended version). arXiv preprint arXiv:1406.7608.

[8]

Benjamin Caulfield, Markus N Rabe, Sanjit A Seshia, and Stavros Tripakis. 2015. What’s Decidable about Syntax-Guided Synthesis? arXiv preprint arXiv:1510.08393.

[9]

Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. 2015. From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. In Computer Aided Verification - 27th International Conference, CAV (Lecture Notes in Computer Science, Vol. 9207). Springer. https://doi.org/10.1007/978-3-319-21668-3_11

[10]

Pavol Černỳ, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. 2014. Regression-free synthesis for concurrency. In International conference on computer aided verification.

Digital Library

[11]

Sarah Chasins and Julie L. Newcomb. 2016. Using SyGuS to Synthesize Reactive Motion Plans. In Proceedings Fifth Workshop on Synthesis (Electronic Proceedings in Theoretical Computer Science, Vol. 229). Open Publishing Association. https://doi.org/10.4204/EPTCS.229.3

[12]

Wonhyuk Choi, Michel Vazirani, and Mark Santolucito. 2021. Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications. In Asian Symposium on Programming Languages and Systems.

[13]

Alonzo Church. 1957. Applications of recursive arithmetic to the problem of circuit synthesis. Summaries of the Summer Institute of Symbolic Logic at Cornell University, Vol. 1.

[14]

Alessandro Cimatti, Marco Roveri, Viktor Schuppan, and Andrei Tchaltsev. 2008. Diagnostic information for realizability. In International Workshop on Verification, Model Checking, and Abstract Interpretation.

[15]

Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In International Conference on Computer Aided Verification.

[16]

Conal Elliott and Paul Hudak. 1997. Functional reactive animation. In Proceedings of the second ACM SIGPLAN international conference on Functional programming.

Digital Library

[17]

Bernd Finkbeiner, Philippe Heim, and Noemi Passing. 2021. Temporal Stream Logic modulo Theories. arxiv:2104.14988. arxiv:2104.14988

[18]

Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. 2019. Synthesizing functional reactive programs. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell.

Digital Library

[19]

Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. 2019. Temporal stream logic: Synthesis beyond the bools. In International Conference on Computer Aided Verification.

[20]

Sumit Gulwani. 2011. Automating String Processing in Spreadsheets using Input-Output Examples. In POPL. https://www.microsoft.com/en-us/research/publication/automating-string-processing-spreadsheets-using-input-output-examples/

[21]

Liana Hadarean, Kshitij Bansal, Dejan Jovanović, Clark Barrett, and Cesare Tinelli. 2014. A tale of two solvers: Eager and lazy approaches to bit-vectors. In International Conference on Computer Aided Verification.

Digital Library

[22]

Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM, 12, 10 (1969).

[23]

Kyle Hsu, Rupak Majumdar, Kaushik Mallik, and Anne-Kathrin Schmuck. 2018. Multi-layered abstraction-based controller synthesis for continuous-time systems. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week).

Digital Library

[24]

Qinheping Hu, Jason Breck, John Cyphert, Loris D’Antoni, and Thomas Reps. 2019. Proving unrealizability for syntax-guided synthesis. In International Conference on Computer Aided Verification.

[25]

Qinheping Hu, John Cyphert, Loris D’Antoni, and Thomas Reps. 2020. Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[26]

Swen Jacobs. 2014. Extended AIGER format for synthesis. arXiv preprint arXiv:1405.5793.

[27]

Swen Jacobs, Felix Klein, and Sebastian Schirmer. 2016. A high-level LTL synthesis format: TLSF v1. 1. arXiv preprint arXiv:1604.02284.

[28]

Swen Jacobs, Guillermo Perez, Roderick Bloem, and Armin Biere. 2020. The 7th Reactive Synthesis Competition. http://www.syntcomp.org/wp-content/uploads/2020/07/SYNTCOMP2020-SYNT.pdf Accessed: 2021-05-18.

[29]

Ron Koymans. 1990. Specifying real-time properties with metric temporal logic. Real-time systems, 2, 4 (1990).

[30]

Shuvendu K Lahiri and Sanjit A Seshia. 2004. The UCLID decision procedure. In International Conference on Computer Aided Verification.

[31]

Robert Love. 2010. Linux kernel development. Pearson Education.

[32]

Parthasarathy Madhusudan. 2011. Synthesizing reactive programs. In Computer Science Logic (CSL’11)-25th International Workshop/20th Annual Conference of the EACSL.

[33]

Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer.

[34]

Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. 2018. Strix: Explicit Reactive Synthesis Strikes Back!. In Computer Aided Verification - 30th International Conference, CAV (Lecture Notes in Computer Science, Vol. 10981). Springer. https://doi.org/10.1007/978-3-319-96145-3_31

[35]

Amir Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science.

Digital Library

[36]

Amir Pnueli and Roni Rosner. 1989. On the Synthesis of an Asynchronous Reactive Module. In Automata, Languages and Programming, 16th International Colloquium (Lecture Notes in Computer Science, Vol. 372). Springer. https://doi.org/10.1007/BFb0035790

[37]

Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray, and Sanjit A. Seshia. 2015. Reactive Synthesis from Signal Temporal Logic Specifications. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC ’15). Association for Computing Machinery, New York, NY, USA. isbn:9781450334334

[38]

Leonid Ryzhyk and Adam Walker. 2016. Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned. In Proceedings Fifth Workshop on Synthesis, SYNT@CAV (EPTCS, Vol. 229). https://doi.org/10.4204/EPTCS.229.8

[39]

David Shah, Eddie Hung, Clifford Wolf, Serge Bazanski, Dan Gisselquist, and Miodrag Milanovic. 2019. Yosys+ nextpnr: an open source framework from verilog to bitstream for commercial fpgas. In IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM).

[40]

Abraham Silberschatz, Peter Baer Galvin, and Greg Gagne. 2014. Operating system concepts essentials.

Cited By

Heim PDimitrova R(2025)Translation of Temporal Logic for Efficient Infinite-State Reactive SynthesisProceedings of the ACM on Programming Languages10.1145/37048889:POPL(1536-1567)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704888
Rodríguez AGorostiaga FSánchez C(2025)Predictable and Performant Reactive Synthesis Modulo Theories via Functional SynthesisAutomated Technology for Verification and Analysis10.1007/978-3-031-78750-8_2(28-50)Online publication date: 12-Feb-2025
https://doi.org/10.1007/978-3-031-78750-8_2
Heim PDimitrova R(2024)Solving Infinite-State Games via AccelerationProceedings of the ACM on Programming Languages10.1145/36328998:POPL(1696-1726)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632899
Show More Cited By

Index Terms

Can reactive synthesis and syntax-guided synthesis be friends?
1. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Can reactive synthesis and syntax-guided synthesis be friends?
SPLASH Companion 2021: Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...
Optimizing synthesis with metasketches
POPL '16

Many advanced programming tools---for both end-users and expert developers---rely on program synthesis to automatically generate implementations from high-level specifications. These tools often need to employ tricky, custom-built synthesis algorithms ...
Syntax-guided synthesis of Datalog programs
ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Datalog has witnessed promising applications in a variety of domains. We propose a programming-by-example system, ALPS, to synthesize Datalog programs from input-output examples. Scaling synthesis to realistic programs in this manner is challenging due ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2022

1038 pages

ISBN:9781450392655

DOI:10.1145/3519939

General Chair:
Ranjit Jhala
University of California at San Diego, USA
,
Program Chair:
Işil Dillig
University of Texas at Austin, USA

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '22

Sponsor:

SIGPLAN

PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 13 - 17, 2022

CA, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
278
Total Downloads

Downloads (Last 12 months)56
Downloads (Last 6 weeks)5

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Heim PDimitrova R(2025)Translation of Temporal Logic for Efficient Infinite-State Reactive SynthesisProceedings of the ACM on Programming Languages10.1145/37048889:POPL(1536-1567)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704888
Rodríguez AGorostiaga FSánchez C(2025)Predictable and Performant Reactive Synthesis Modulo Theories via Functional SynthesisAutomated Technology for Verification and Analysis10.1007/978-3-031-78750-8_2(28-50)Online publication date: 12-Feb-2025
https://doi.org/10.1007/978-3-031-78750-8_2
Heim PDimitrova R(2024)Solving Infinite-State Games via AccelerationProceedings of the ACM on Programming Languages10.1145/36328998:POPL(1696-1726)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632899
Amir GMaayan OZelazny TKatz GSchapira M(2024)Verifying the Generalization of Deep Learning to Out-of-Distribution DomainsJournal of Automated Reasoning10.1007/s10817-024-09704-768:3Online publication date: 3-Aug-2024
https://doi.org/10.1007/s10817-024-09704-7
Maderbacher BWindisch FBloem R(2024)Synthesis from Infinite-State Generalized Reactivity(1) SpecificationsLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_17(281-301)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_17
Schmuck AHeim PDimitrova RNayak S(2024)Localized Attractor Computations for Infinite-State GamesComputer Aided Verification10.1007/978-3-031-65633-0_7(135-158)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_7
Das RTenenbaum JSolar-Lezama ATavares Z(2023)Combining Functional and Automata Synthesis to Discover Causal Reactive ProgramsProceedings of the ACM on Programming Languages10.1145/35712497:POPL(1628-1658)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571249
Coenen NFinkbeiner BHofmann JTillman J(2023)Smart Contract Synthesis Modulo Hyperproperties2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00006(276-291)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00006
Samuel SD'Souza DKomondoor R(2023)Symbolic Fixpoint Algorithms for Logical LTL Games2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE56229.2023.00212(698-709)Online publication date: 11-Sep-2023
https://doi.org/10.1109/ASE56229.2023.00212

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten