research-article

Growing solver-aided languages with rosette

Authors:

Rastislav BodikAuthors Info & Claims

Onward! 2013: Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software

Pages 135 - 152

https://doi.org/10.1145/2509578.2509586

Published: 29 October 2013 Publication History

Abstract

SAT and SMT solvers have automated a spectrum of programming tasks, including program synthesis, code checking, bug localization, program repair, and programming with oracles. In principle, we obtain all these benefits by translating the program (once) to a constraint system understood by the solver. In practice, however, compiling a language to logical formulas is a tricky process, complicated by having to map the solution back to the program level and extend the language with new solver-aided constructs, such as symbolic holes used in synthesis.

This paper introduces ROSETTE, a framework for designing solver-aided languages. ROSETTE is realized as a solver-aided language embedded in Racket, from which it inherits extensive support for meta-programming. Our framework frees designers from having to compile their languages to constraints: new languages, and their solver-aided constructs, are defined by shallow (library-based) or deep (interpreter-based) embedding in ROSETTE itself.

We describe three case studies, by ourselves and others, of using ROSETTE to implement languages and synthesizers for web scraping, spatial programming, and superoptimization of bitvector programs.

References

[1]

A. Aavani. Translating pseudo-boolean constraints into CNF. In Theory and Application of Satisfiability Testing (SAT), 2011.

Digital Library

[2]

P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2000.

Digital Library

[3]

AIGER. fmv.jku.at/aiger/.

[4]

Al-Anon AR Meetings. www.ar.al-anon.alateen.org/alanonmeetings.htm.

[5]

M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), 2004.

Digital Library

[6]

Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification. www.eecs.berkeley.edu/~alanmi/abc/.

[7]

S. Chandra, E. Torlak, S. Barman, and R. Bodik. Angelic debugging. In Intl. Conf. on Software Engineering (ICSE), 2011.

Digital Library

[8]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2004.

[9]

G. Dennis. A relational framework for bounded program verification. PhD thesis, Massachusetts Institute of Technology, 2009.

[10]

G. Dennis, F. S.-H. Chang, and D. Jackson. Modular verification of code with SAT. In Intl. Symp. on Software Testing and Analysis (ISSTA), 2006.

Digital Library

[11]

G. Dennis, F. S.-H. Chang, and D. Jackson. Modular verification of code with SAT. In Intl. Symp. on Software Testing and Analysis (ISSTA), 2006.

Digital Library

[12]

J. Dolby, M. Vaziri, and F. Tip. Finding bugs efficiently with a SAT solver. In Foundations of Software Engineering (FSE), 2007.

Digital Library

[13]

M. Felleisen. The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987.

Digital Library

[14]

M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. The MIT Press, 1st edition, 2009. ISBN 0262062755, 9780262062756.

Digital Library

[15]

J. Galeotti, N. Rosner, C. Pombo, and M. Frias. Analysis of invariants for efficient bounded verification. In Intl. Symp. on Software Testing and Analysis (ISSTA), 2010.

Digital Library

[16]

J. P. Galeotti. Software Verification Using Alloy. PhD thesis, University of Buenos Aires, 2010.

[17]

S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In Programming Language Design and Implementation (PLDI), 2011.

Digital Library

[18]

IMDb Top 250 movies. www.imdb.com/chart/top.

[19]

iTunes Top 100 Songs. www.apple.com/itunes/charts/songs/.

[20]

P. Jackson and D. Sheridan. Clause form conversions for boolean circuits. In Theory and Application of Satisfiability Testing (SAT), 2005.

Digital Library

[21]

JavaPathFinder. babelfish.arc.nasa.gov/trac/jpf/.

[22]

M. Jose and R. Majumdar. Bug-Assist: assisting fault localization in ansi-c programs. In Computer Aided Verification (CAV) verification, 2011.

Digital Library

[23]

A. S. Köksal, V. Kuncak, and P. Suter. Constraints as control. In Principles of Programming Languages (POPL), 2012.

Digital Library

[24]

K. R. M. Leino. Dafny: an automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2010.

Digital Library

[25]

K. R. M. Leino and P. Rümmer. A polymorphic intermediate verification language: Design and logical encoding. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2010.

Digital Library

[26]

A. Milicevic. Executable specifications for Java programs. Master's thesis, Massachusetts Institute of Technology, 2010.

[27]

J. P. Near and D. Jackson. Rubicon: bounded verification of web applications. In Foundations of Software Engineering (FSE), 2012.

Digital Library

[28]

R. Nokhbeh Zaeem and S. Khurshid. Contract-based data structure repair using Alloy. In European Conf. on Object-Oriented Programming (ECOOP), 2010.

Digital Library

[29]

R. Nokhbeh Zaeem, D. Gopinath, S. Khurshid, and K. S. McKinley. History-aware data structure repair using SAT. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012.

Digital Library

[30]

J. D. Ramsdell. An operational semantics for Scheme. SIGPLAN Lisp Pointers, V(2):6--10, 1992.

Digital Library

[31]

H. Samimi and K. Rajan. Specification-based sketching with Sketch#. In Workshop on Formal Techniques for Java-Like Programs (FTfJP), 2011.

Digital Library

[32]

H. Samimi, E. D. Aung, and T. Millstein. Falling back on executable specifications. In European Conf. on Object-Oriented Programming (ECOOP), 2010.

Digital Library

[33]

J. H. Siddiqui and S. Khurshid. Symbolic execution of Alloy models. In Intl. Conf. on Formal Methods and Software Engineering (ICFEM), 2011.

Digital Library

[34]

A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. A. Seshia. Combinatorial sketching for finite programs. In Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2006.

Digital Library

[35]

P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive programs. In Static Analysis Symp. (SAS), 2011.

Digital Library

[36]

M. Taghdiri. Automating Modular Program Verification by Refining Specifications. PhD thesis, Massachusetts Institute of Technology, 2007.

Digital Library

[37]

M. Taghdiri. Automating Modular Program Verification by Refining Specifications. PhD thesis, Massachusetts Institute of Technology, 2007.

Digital Library

[38]

R. Tate, M. Stepp, and S. Lerner. Generating compiler optimizations from proofs. In Principles of Programming Languages (POPL), 2010.

Digital Library

[39]

The Racket Programming Language. racket-lang.org.

[40]

E. Torlak, M. Vaziri, and J. Dolby. MemSAT: checking axiomatic specifications of memory models. In Programming Language Design and Implementation (PLDI), 2010.

Digital Library

[41]

W.Weimer, S. Forrest, C. L. Goues, and T. Nguyen. Automatic program repair with evolutionary computation. Commun. ACM, 53(5):109--116, 2010.

Digital Library

[42]

XPath. XML Path Language. www.w3.org/TR/xpath/.

[43]

D. Yoo. Fudging up Racket. hashcollision.org/brainfudge.

Cited By

Liu ZMada SRegehr J(2024)Minotaur: A SIMD-Oriented Synthesizing SuperoptimizerProceedings of the ACM on Programming Languages10.1145/36897668:OOPSLA2(1561-1585)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689766
Bragg NFoster JZucker PEdwards JTaeumel M(2024)Scimitar: Functional Programs as Optimization ProblemsProceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3689492.3690051(96-112)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689492.3690051
Lee YGopinathan KYang ZFlatt MSergey ILaemmel RPereira JMosses P(2024)DSLs in Racket: You Want It How, Now?Proceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3687997.3695645(84-103)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3687997.3695645
Show More Cited By

Index Terms

Growing solver-aided languages with rosette
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Software implementation planning
        Software design techniques
    2. Software development process management
  2. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

A lightweight symbolic virtual machine for solver-aided host languages
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

Solver-aided domain-specific languages (SDSLs) are an emerging class of computer-aided programming systems. They ease the construction of programs by using satisfiability solvers to automate tasks such as verification, debugging, synthesis, and non-...
A lightweight symbolic virtual machine for solver-aided host languages
PLDI '14

Solver-aided domain-specific languages (SDSLs) are an emerging class of computer-aided programming systems. They ease the construction of programs by using satisfiability solvers to automate tasks such as verification, debugging, synthesis, and non-...
Growing languages with metamorphic syntax macros
PEPM '02: Proceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation

"From now on, a main goal in designing a language should be to plan for growth." Guy Steele: Growing a Language, OOPSLA '98 invited talk.We present our experiences with a syntax macro language which we claim forms a general abstraction mechanism for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

Onward! 2013: Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software

October 2013

218 pages

ISBN:9781450324724

DOI:10.1145/2509578

General Chairs:
Anthony Hosking
Purdue University, USA
,
Patrick Eugster
Purdue University, USA
,
Program Chair:
Robert Hirschfeld
Hasso-Plattner-Institute, University of Potsdam, Germany

Copyright © 2013 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 the author(s) 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: 29 October 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tag

solver-aided languages

Qualifiers

Research-article

Conference

SPLASH '13

Sponsor:

SIGPLAN

SPLASH '13: Conference on Systems, Programming, and Applications: Software for Humanity

October 29 - 31, 2013

Indiana, Indianapolis, USA

Acceptance Rates

Onward! 2013 Paper Acceptance Rate 11 of 27 submissions, 41%;

Overall Acceptance Rate 40 of 105 submissions, 38%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

158
Total Citations
View Citations
780
Total Downloads

Downloads (Last 12 months)214
Downloads (Last 6 weeks)22

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu ZMada SRegehr J(2024)Minotaur: A SIMD-Oriented Synthesizing SuperoptimizerProceedings of the ACM on Programming Languages10.1145/36897668:OOPSLA2(1561-1585)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689766
Bragg NFoster JZucker PEdwards JTaeumel M(2024)Scimitar: Functional Programs as Optimization ProblemsProceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3689492.3690051(96-112)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689492.3690051
Lee YGopinathan KYang ZFlatt MSergey ILaemmel RPereira JMosses P(2024)DSLs in Racket: You Want It How, Now?Proceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3687997.3695645(84-103)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3687997.3695645
Lu DTang BPaper MKogias M(2024)Towards Functional Verification of eBPF ProgramsProceedings of the ACM SIGCOMM 2024 Workshop on eBPF and Kernel Extensions10.1145/3672197.3673435(37-43)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672197.3673435
Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Ji RZhao YPolikarpova NXiong YHu Z(2024)Superfusion: Eliminating Intermediate Data Structures via Inductive SynthesisProceedings of the ACM on Programming Languages10.1145/36564158:PLDI(939-964)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656415
Hong QAiken A(2024)Recursive Program Synthesis using ParamorphismsProceedings of the ACM on Programming Languages10.1145/36563818:PLDI(102-125)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656381
Hung HAmiri Sani A(2024)BRF: Fuzzing the eBPF RuntimeProceedings of the ACM on Software Engineering10.1145/36437781:FSE(1152-1171)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643778
Mei YJones BCascaval DMankoff JVouga ESchulz A(2024)FabHacks: Transform Everyday Objects into Home Hacks Leveraging a Solver-aided DSLProceedings of the 9th ACM Symposium on Computational Fabrication10.1145/3639473.3665788(1-16)Online publication date: 7-Jul-2024
https://dl.acm.org/doi/10.1145/3639473.3665788
Deng HTao RPeng YWu X(2024)A Case for Synthesis of Recursive Quantum Unitary ProgramsProceedings of the ACM on Programming Languages10.1145/36329018:POPL(1759-1788)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632901
Show More Cited By

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents