More Web Proxy on the site http://driver.im/

research-article

Open access

Grisette: Symbolic Compilation as a Functional Programming Library

Authors:

Rastislav BodíkAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL

Article No.: 16, Pages 455 - 487

https://doi.org/10.1145/3571209

Published: 11 January 2023 Publication History

Abstract

The development of constraint solvers simplified automated reasoning about programs and shifted the engineering burden to implementing symbolic compilation tools that translate programs into efficiently solvable constraints. We describe Grisette, a reusable symbolic evaluation framework for implementing domain-specific symbolic compilers. Grisette evaluates all execution paths and merges their states into a normal form that avoids making guards mutually exclusive. This ordered-guards representation reduces the constraint size 5-fold and the solving time more than 2-fold. Grisette is designed entirely as a library, which sidesteps the complications of lifting the host language into the symbolic domain. Grisette is purely functional, enabling memoization of symbolic compilation as well as monadic integration with host libraries. Grisette is statically typed, which allows catching programming errors at compile time rather than delaying their detection to the constraint solver. We implemented Grisette in Haskell and evaluated it on benchmarks that stress both the symbolic evaluation and constraint solving.

References

[1]

Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. Springer International Publishing, Cham. 249–272. isbn:978-3-319-30936-1 https://doi.org/10.1007/978-3-319-30936-1_14

[2]

Krste Asanović and David A Patterson. 2014. Instruction sets should be free: The case for risc-v. EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2014-146.

[3]

Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, and David Brumley. 2014. Enhancing Symbolic Execution with Veritesting. In Proceedings of the 36th International Conference on Software Engineering (ICSE 2014). Association for Computing Machinery, New York, NY, USA. 1083–1094. isbn:9781450327565 https://doi.org/10.1145/2568225.2568293

Digital Library

[4]

Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques. ACM Comput. Surv., 51, 3 (2018), Article 50, may, 39 pages. issn:0360-0300 https://doi.org/10.1145/3182657

Digital Library

[5]

Mike Barnett, K Rustan M Leino, and Wolfram Schulte. 2004. The Spec# programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. 49–69. https://doi.org/10.1007/978-3-540-30569-9_3

Digital Library

[6]

Régis William Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter. 2013. On Verification by Translation to Recursive Functions.

[7]

James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. 2016. Specifying and Checking File System Crash-Consistency Models. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’16). Association for Computing Machinery, New York, NY, USA. 83–98. isbn:9781450340915 https://doi.org/10.1145/2872362.2872406

Digital Library

[8]

James Bornholt and Emina Torlak. 2018. Finding Code That Explodes under Symbolic Evaluation. Proc. ACM Program. Lang., 2, OOPSLA (2018), Article 149, oct, 26 pages. https://doi.org/10.1145/3276519

Digital Library

[9]

Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. 1975. SELECT—a Formal System for Testing and Debugging Programs by Symbolic Execution. In Proceedings of the International Conference on Reliable Software. Association for Computing Machinery, New York, NY, USA. 234–245. isbn:9781450373852 https://doi.org/10.1145/800027.808445

Digital Library

[10]

Robert Brummayer and Armin Biere. 2009. Boolector: An efficient SMT solver for bit-vectors and arrays. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 174–177. https://doi.org/10.1007/978-3-642-00768-2_16

Digital Library

[11]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI’08). USENIX Association, USA. 209–224.

Digital Library

[12]

Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. 2008. EXE: Automatically Generating Inputs of Death. ACM Trans. Inf. Syst. Secur., 12, 2 (2008), Article 10, dec, 38 pages. issn:1094-9224 https://doi.org/10.1145/1455518.1455522

Digital Library

[13]

Kartik Chandra and Rastislav Bodik. 2017. Bonsai: Synthesis-Based Reasoning for Type Systems. Proc. ACM Program. Lang., 2, POPL (2017), Article 62, dec, 34 pages. https://doi.org/10.1145/3158150

Digital Library

[14]

Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017. Cosette: An Automated Prover for SQL. In CIDR.

[15]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems, Kurt Jensen and Andreas Podelski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 168–176. isbn:978-3-540-24730-2 https://doi.org/10.1007/978-3-540-24730-2_15

[16]

Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming (LFP ’90). Association for Computing Machinery, New York, NY, USA. 151–160. isbn:089791368X https://doi.org/10.1145/91556.91622

Digital Library

[17]

David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn. 2017. Abstracting Definitional Interpreters (Functional Pearl). Proc. ACM Program. Lang., 1, ICFP (2017), Article 12, aug, 25 pages. https://doi.org/10.1145/3110256

Digital Library

[18]

N.G de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75, 5 (1972), 381–392. issn:1385-7258 https://doi.org/10.1016/1385-7258(72)90034-0

[19]

Leonardo De Moura and Nikolaj Bjørner. 2011. Satisfiability modulo Theories: Introduction and Applications. Commun. ACM, 54, 9 (2011), sep, 69–77. issn:0001-0782 https://doi.org/10.1145/1995376.1995394

Digital Library

[20]

Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. 2006. Modular Verification of Code with SAT. In Proceedings of the 2006 International Symposium on Software Testing and Analysis (ISSTA ’06). Association for Computing Machinery, New York, NY, USA. 109–120. isbn:1595932631 https://doi.org/10.1145/1146238.1146251

Digital Library

[21]

Julian Dolby, Mandana Vaziri, and Frank Tip. 2007. Finding Bugs Efficiently with a SAT Solver. In Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering (ESEC-FSE ’07). Association for Computing Machinery, New York, NY, USA. 195–204. isbn:9781595938114 https://doi.org/10.1145/1287624.1287653

Digital Library

[22]

Conal Elliott. 2017. Compiling to Categories. Proc. ACM Program. Lang., 1, ICFP (2017), Article 27, aug, 27 pages. https://doi.org/10.1145/3110271

Digital Library

[23]

Patrice Godefroid. 2007. Compositional Dynamic Test Generation. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’07). Association for Computing Machinery, New York, NY, USA. 47–54. isbn:1595935754 https://doi.org/10.1145/1190216.1190226

Digital Library

[24]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed Automated Random Testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’05). Association for Computing Machinery, New York, NY, USA. 213–223. isbn:1595930566 https://doi.org/10.1145/1065010.1065036

Digital Library

[25]

William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac. 2019. Lazy Counterfactual Symbolic Execution. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA. 411–424. isbn:9781450367127 https://doi.org/10.1145/3314221.3314618

Digital Library

[26]

William T. Hallahan, Anton Xue, and Ruzica Piskac. 2019. G2Q: Haskell Constraint Solving. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell (Haskell 2019). Association for Computing Machinery, New York, NY, USA. 44–57. isbn:9781450368131 https://doi.org/10.1145/3331545.3342590

Digital Library

[27]

Trevor Hansen, Peter Schachte, and Harald Søndergaard. 2009. State Joining and Splitting for the Symbolic Execution of Binaries. In Runtime Verification, Saddek Bensalem and Doron A. Peled (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 76–92. isbn:978-3-642-04694-0 https://doi.org/10.1007/978-3-642-04694-0_6

Digital Library

[28]

Klaus Havelund and Thomas Pressburger. 2000. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 2, 4 (2000), 366–381. https://doi.org/10.1007/s100090050043

[29]

Joe Hermaszewski. 2021. vector-sized. https://hackage.haskell.org/package/vector-sized

[30]

Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. 2010. Oracle-Guided Component-Based Program Synthesis. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1 (ICSE ’10). Association for Computing Machinery, New York, NY, USA. 215–224. isbn:9781605587196 https://doi.org/10.1145/1806799.1806833

Digital Library

[31]

James Cornelius. King. 1969. A program verifier. Ph. D. Dissertation. lccn:76127837

[32]

James C. King. 1975. A New Approach to Program Testing. In Proceedings of the International Conference on Reliable Software. Association for Computing Machinery, New York, NY, USA. 228–233. isbn:9781450373852 https://doi.org/10.1145/800027.808444

Digital Library

[33]

James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM, 19, 7 (1976), jul, 385–394. issn:0001-0782 https://doi.org/10.1145/360248.360252

Digital Library

[34]

Oleg Kiselyov. 2013. Efficient Set Monad. https://web.archive.org/web/20201112030922/http://okmij.org/ftp/Haskell/set-monad.html archived 2020-11-12

[35]

Oleg Kiselyov, Amr Sabry, and Cameron Swords. 2013. Extensible Effects: An Alternative to Monad Transformers. In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell (Haskell ’13). Association for Computing Machinery, New York, NY, USA. 59–70. isbn:9781450323833 https://doi.org/10.1145/2503778.2503791

Digital Library

[36]

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. 2012. Constraints as Control. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12). Association for Computing Machinery, New York, NY, USA. 151–164. isbn:9781450310833 https://doi.org/10.1145/2103656.2103675

Digital Library

[37]

Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. 2012. Efficient State Merging in Symbolic Execution. 193–204. isbn:9781450312059 https://doi.org/10.1145/2254064.2254088

Digital Library

[38]

Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization, 2004. CGO 2004. 75–86. https://doi.org/10.1109/CGO.2004.1281665

[39]

K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. 348–370. https://doi.org/10.1007/978-3-642-17511-4_20

[40]

K Rustan M Leino and Philipp Rümmer. 2010. A polymorphic intermediate verification language: Design and logical encoding. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 312–327. https://doi.org/10.1007/978-3-642-12002-2_26

Digital Library

[41]

Sergey Mechtaev, Jooyong Yi, and Abhik Roychoudhury. 2016. Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis. In Proceedings of the 38th International Conference on Software Engineering (ICSE ’16). Association for Computing Machinery, New York, NY, USA. 691–701. isbn:9781450339001 https://doi.org/10.1145/2884781.2884807

Digital Library

[42]

Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser. 2019. From Definitional Interpreter to Symbolic Executor. In Proceedings of the 4th ACM SIGPLAN International Workshop on Meta-Programming Techniques and Reflection (META 2019). Association for Computing Machinery, New York, NY, USA. 11–20. isbn:9781450369855 https://doi.org/10.1145/3358502.3361269

Digital Library

[43]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

[44]

Joseph P. Near and Daniel Jackson. 2012. Rubicon: Bounded Verification of Web Applications. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE ’12). Association for Computing Machinery, New York, NY, USA. Article 60, 11 pages. isbn:9781450316149 https://doi.org/10.1145/2393596.2393667

Digital Library

[45]

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP ’19). Association for Computing Machinery, New York, NY, USA. 225–242. isbn:9781450368735 https://doi.org/10.1145/3341301.3359641

Digital Library

[46]

Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak. 2022. A Formal Foundation for Symbolic Evaluation with Merging. Proc. ACM Program. Lang., 6, POPL (2022), Article 47, jan, 28 pages. https://doi.org/10.1145/3498709

Digital Library

[47]

Richard L Rudell. 1986. Multiple-valued logic minimization for PLA synthesis. CALIFORNIA UNIV BERKELEY ELECTRONICS RESEARCH LAB.

[48]

Neil Sculthorpe, Jan Bracker, George Giorgidze, and Andy Gill. 2013. The Constrained-Monad Problem. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). Association for Computing Machinery, New York, NY, USA. 287–298. isbn:9781450323260 https://doi.org/10.1145/2500365.2500602

Digital Library

[49]

Koushik Sen, Swaroop Kalasapur, Tasneem Brutch, and Simon Gibbs. 2013. Jalangi: A Selective Record-Replay and Dynamic Analysis Framework for JavaScript. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2013). Association for Computing Machinery, New York, NY, USA. 488–498. isbn:9781450322379 https://doi.org/10.1145/2491411.2491447

Digital Library

[50]

Koushik Sen, George Necula, Liang Gong, and Wontae Choi. 2015. MultiSE: Multi-Path Symbolic Execution Using Value Summaries. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2015). Association for Computing Machinery, New York, NY, USA. 842–853. isbn:9781450336758 https://doi.org/10.1145/2786805.2786830

Digital Library

[51]

Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, and Willem Visser. 2020. Java Ranger: Statically Summarizing Regions for Efficient Symbolic Execution of Java. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020). Association for Computing Machinery, New York, NY, USA. 123–134. isbn:9781450370431 https://doi.org/10.1145/3368089.3409734

Digital Library

[52]

Tim Sheard and Simon Peyton Jones. 2002. Template Meta-Programming for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell (Haskell ’02). Association for Computing Machinery, New York, NY, USA. 1–16. isbn:1581136056 https://doi.org/10.1145/581690.581691

Digital Library

[53]

Nishant Sinha. 2008. Symbolic Program Analysis Using Term Rewriting and Generalization. In 2008 Formal Methods in Computer-Aided Design. 1–9. https://doi.org/10.1109/FMCAD.2008.ECP.23

[54]

Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph. D. Dissertation. USA. isbn:9781109097450 AAI3353225

[55]

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XII). Association for Computing Machinery, New York, NY, USA. 404–415. isbn:1595934510 https://doi.org/10.1145/1168857.1168907

Digital Library

[56]

Don Stewart and Duncan Coutts. 2021. bytestring. https://hackage.haskell.org/package/bytestring

[57]

Mads Tofte. 1990. Type inference for polymorphic references. Information and Computation, 89, 1 (1990), 1–34. issn:0890-5401 https://doi.org/10.1016/0890-5401(90)90018-D

Digital Library

[58]

Emina Torlak. 2016. unsound behavior? https://web.archive.org/web/20201122222820/https://github.com/emina/rosette/issues/36 archived 2020-11-22

[59]

Emina Torlak. 2021. Use early return in rosette? https://web.archive.org/web/20220223043310/https://github.com/emina/rosette/issues/201 archived 2022-02-22

[60]

Emina Torlak. 2022. Debugging, Rosette Guide. https://web.archive.org/web/20220520032819/https://docs.racket-lang.org/rosette-guide/ch_error-tracing.html##%28part._sec~3aerrors-in-rosette%29 archived 2022-05-20

[61]

Emina Torlak and Rastislav Bodik. 2013. Growing Solver-Aided Languages with Rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward! 2013). Association for Computing Machinery, New York, NY, USA. 135–152. isbn:9781450324724 https://doi.org/10.1145/2509578.2509586

Digital Library

[62]

Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14). Association for Computing Machinery, New York, NY, USA. 530–541. isbn:9781450327848 https://doi.org/10.1145/2594291.2594340

Digital Library

[63]

Richard Uhler and Nirav Dave. 2013. Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 678–683. isbn:978-3-642-39799-8 https://doi.org/10.1007/978-3-642-39799-8_45

[64]

Richard Uhler and Nirav Dave. 2014. Smten with Satisfiability-Based Search. 157–176. isbn:9781450325851 https://doi.org/10.1145/2660193.2660208

Digital Library

[65]

Guannan Wei, Oliver Bračevac, Shangyin Tan, and Tiark Rompf. 2020. Compiling Symbolic Execution with Staging and Algebraic Effects. Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 164, nov, 33 pages. https://doi.org/10.1145/3428232

Digital Library

[66]

Max Willsey, Ashley P. Stephenson, Chris Takahashi, Pranav Vaid, Bichlien H. Nguyen, Michal Piszczek, Christine Betts, Sharon Newman, Sarang Joshi, Karin Strauss, and Luis Ceze. 2019. Puddle: A Dynamic, Error-Correcting, Full-Stack Microfluidics Platform. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’19). Association for Computing Machinery, New York, NY, USA. 183–197. isbn:9781450362405 https://doi.org/10.1145/3297858.3304027

Digital Library

[67]

A.K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, 115, 1 (1994), 38–94. issn:0890-5401 https://doi.org/10.1006/inco.1994.1093

Digital Library

[68]

Nicolas Wu and Tom Schrijvers. 2015. Fusion for Free. In Mathematics of Program Construction, Ralf Hinze and Janis Voigtländer (Eds.). Springer International Publishing, Cham. 302–322. isbn:978-3-319-19797-5 https://doi.org/10.1007/978-3-319-19797-5_15

[69]

Nicolas Wu, Tom Schrijvers, Rob Rix, and Patrick Thomson. 2022. fused-effects. https://hackage.haskell.org/package/fused-effects

[70]

Yichen Xie and Alex Aiken. 2005. Scalable Error Detection Using Boolean Satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’05). Association for Computing Machinery, New York, NY, USA. 351–363. isbn:158113830X https://doi.org/10.1145/1040305.1040334

Digital Library

Cited By

Arora JLu SJain DXu THoushmand FPhothilimthana PLesani MNarayanan PMurthy KBodik RSabne AMendis C(2025)TensorRight: Automated Verification of Tensor Graph RewritesProceedings of the ACM on Programming Languages10.1145/37048659:POPL(832-863)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704865
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
Ji RZhao YXiong YWang DZhang LHu Z(2024)Decomposition-based Synthesis for Applying Divide-and-Conquer-like Algorithmic ParadigmsACM Transactions on Programming Languages and Systems10.1145/364844046:2(1-59)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3648440

Index Terms

Grisette: Symbolic Compilation as a Functional Programming Library
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Logic
    1. Automated reasoning

Recommendations

Tree traversal synthesis using domain-specific symbolic compilation
ASPLOS '22: Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems

Efficient computation on tree data structures is important in compilers, numeric computations, and web browser layout engines. Efficiency is achieved by statically scheduling the computation into a small number of tree traversals and by performing the ...
A formal foundation for symbolic evaluation with merging

Reusable symbolic evaluators are a key building block of solver-aided verification and synthesis tools. A reusable evaluator reduces the semantics of all paths in a program to logical constraints, and a client tool uses these constraints to formulate a ...
Meta-compilation of language abstractions

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue POPL

January 2023

2196 pages

EISSN:2475-1421

DOI:10.1145/3554308

Editor:

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023

Published in PACMPL Volume 7, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
742
Total Downloads

Downloads (Last 12 months)288
Downloads (Last 6 weeks)41

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Arora JLu SJain DXu THoushmand FPhothilimthana PLesani MNarayanan PMurthy KBodik RSabne AMendis C(2025)TensorRight: Automated Verification of Tensor Graph RewritesProceedings of the ACM on Programming Languages10.1145/37048659:POPL(832-863)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704865
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
Ji RZhao YXiong YWang DZhang LHu Z(2024)Decomposition-based Synthesis for Applying Divide-and-Conquer-like Algorithmic ParadigmsACM Transactions on Programming Languages and Systems10.1145/364844046:2(1-59)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3648440

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents