research-article

Open access

Bonsai: synthesis-based reasoning for type systems

Authors:

Kartik Chandra,

Rastislav BodikAuthors Info & Claims

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

Article No.: 62, Pages 1 - 34

https://doi.org/10.1145/3158150

Published: 27 December 2017 Publication History

Abstract

When designing a type system, we may want to mechanically check the design to guide its further development. We describe algorithms that perform symbolic reasoning about executable models of type systems. The algorithms support three queries. First, they check type soundness and synthesize a counterexample program if such a soundness bug is found. Second, they compare two versions of a type system, synthesizing a program accepted by one but rejected by the other. Third, they minimize the size of synthesized counterexample programs.

These algorithms symbolically evaluate typecheckers and interpreters, producing formulas that characterize the set of programs that fail or succeed in the typechecker and the interpreter. However, symbolically evaluating interpreters poses efficiency challenges, which are caused by having to merge execution paths of the various possible input programs. Our main contribution is the bonsai tree, a novel symbolic representation of programs and program states that addresses these challenges. Bonsai trees encode complex syntactic information in terms of logical constraints, enabling more efficient merging.

We implement these algorithms in the Bonsai tool, an assistant for type system designers. We perform case studies on how Bonsai helps test and explore a variety of type systems. Bonsai efficiently synthesizes counterexamples for soundness bugs previously inaccessible to automatic tools and is the first automated tool to find a counterexample for the recently discovered Scala soundness bug SI-9633.

Supplementary Material

WEBM File (bonsaisynthesis.webm)

Download
113.99 MB

References

[1]

B. Alpern, M. N. Wegman, and F. K. Zadeck. Detecting equality of variables in programs. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’88, pages 1–11, New York, NY, USA, 1988. ACM. ISBN 0-89791-252-7. URL

Digital Library

[2]

Nada Amin and Ross Tate. Java and scala’s type systems are unsound: The existential crisis of null pointers. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pages 838–848, New York, NY, USA, 2016a. ACM. ISBN 978-1-4503-4444-9. URL

Digital Library

[3]

Nada Amin and Ross Tate. Soundness issue with path-dependent type on ‘null‘ path. https://issues.scala-lang.org/browse/SI-9633, 2016b.

[4]

Nada Amin, Tiark Rompf, and Martin Odersky. Foundations of path-dependent types. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’14, pages 233–249, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2585-1. URL

Digital Library

[5]

Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The Essence of Dependent Object Types, pages 249–272. Springer International Publishing, Cham, 2016. ISBN 978-3-319-30936-1. URL

[6]

Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid, and Darko Marinov. Evaluating the “small scope hypothesis". Technical report, MIT Laboratory for Computer Science, 2003.

[7]

Dana Angluin and Carl H. Smith. Inductive inference: Theory and methods. ACM Comput. Surv., 15(3):237–269, 1983.

Digital Library

[8]

Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs. In Klaus Havelund, John Penix, and Willem Visser, editors, SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30 - September 1, 2000, Proceedings, volume 1885 of Lecture Notes in Computer Science, pages 113–130. Springer, 2000. ISBN 3-540-41030-9. URL

[9]

Rastislav Bodík, Kartik Chandra, Phitchaya Mangpo Phothilimthana, and Nathaniel Yazdani. Domain-specific symbolic compilation. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA, volume 71 of LIPIcs, pages 2:1–2:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. ISBN 978-3-95977-032-3. URL

[10]

Chandrasekhar Boyapati. SafeJava: A Unified Type System for Safe Programming. PhD thesis, Massachusetts Institute of Technology, February 2004.

Digital Library

[11]

Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA ’02, pages 211–230, New York, NY, USA, 2002. ACM. ISBN 1-58113-471-1. URL

Digital Library

[12]

Chandrasekhar Boyapati, Barbara Liskov, and Liuba Shrira. Ownership types for object encapsulation. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’03, pages 213–223, New York, NY, USA, 2003. ACM. ISBN 1-58113-628-5. URL

Digital Library

[13]

Lori A. Clarke and Debra J. Richardson. Applications of symbolic evaluation. Journal of Systems and Software, 5(1):15–35, 1985. URL

Digital Library

[14]

W. R. Cook. A proposal for making Eiffel type-safe. Comput. J., 32(4):305–311, July 1989. ISSN 0010-4620. URL

Digital Library

[15]

Manuvir Das, Sorin Lerner, and Mark Seigle. ESP: path-sensitive program verification in polynomial time. In Jens Knoop and Laurie J. Hendren, editors, Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, pages 57–68. ACM, 2002. ISBN 1-58113-463-0. URL

Digital Library

[16]

Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular verification of code with SAT. In International Symposium on Software Testing and Analysis (ISSTA’06), 2006.

Digital Library

[17]

Kyle Dewey, Jared Roesch, and Ben Hardekopf. Language fuzzing using constraint logic programming. In Ivica Crnkovic, Marsha Chechik, and Paul Grünbacher, editors, ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, Vasteras, Sweden - September 15 - 19, 2014, pages 725–730. ACM, 2014. ISBN 978-1-4503-3013-8. URL

Digital Library

[18]

Kyle Dewey, Jared Roesch, and Ben Hardekopf. Fuzzing the Rust typechecker using CLP. In Proceedings of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), ASE ’15, pages 482–493, Washington, DC, USA, 2015. IEEE Computer Society. ISBN 978-1-5090-0025-8. URL

Digital Library

[19]

J. Dolby, M. Vaziri, and F. Tip. Finding bugs efficiently with a sat solver. In 6th International Symposium on the Foundations of Software Engineering (FSE’07), page 204. ACM, 2007.

Digital Library

[20]

Sophia Drossopoulou and Susan Eisenbach. Java is type safe - probably. In In European Conference On Object Oriented Programming, pages 389–418. Springer-Verlag, 1997.

[21]

Burke Fetscher, Koen Claessen, Michal H. Palka, John Hughes, and Robert Bruce Findler. Making random judgments: Automatically generating well-typed terms from the definition of a type-system. In Jan Vitek, editor, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9032 of Lecture Notes in Computer Science, pages 383–405. Springer, 2015. ISBN 978-3-662-46668-1. URL

[22]

Bernd Fischer and Johann Schumann. Autobayes: a system for generating data analysis programs from statistical models. J. Funct. Program., 13(3):483–508, 2003. ISSN 0956-7968.

Digital Library

[23]

Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 193–205. ACM, 2001a. ISBN 1-58113-336-7. URL

Digital Library

[24]

Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: Generating compact verification conditions. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’01, pages 193–205, New York, NY, USA, 2001b. ACM. ISBN 1-58113-336-7. URL

Digital Library

[25]

Matthew Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010-1, PLT Design Inc., 2010. https://racket-lang.org/tr1/ .

[26]

Matteo Frigo and Steven G. Johnson. The design and implementation of FFTW3. Proceedings of the IEEE, 93(2):216–231, 2005. Special issue on “Program Generation, Optimization, and Platform Adaptation”.

[27]

J.P. Galeotti, N. Rosner, C.G.L. Pombo, and M.F. Frias. Analysis of invariants for efficient bounded verification. In 2010 International Symposium on Software Testing and Analysis (ISSTA’10), 2010.

Digital Library

[28]

Sumit Gulwani. Automating string processing in spreadsheets using input-output examples. In POPL, pages 317–330, 2011.

Digital Library

[29]

L. Howard Holley and Barry K. Rosen. Qualified data flow problems. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’80, pages 68–82, New York, NY, USA, 1980. ACM. ISBN 0-89791-011-7. URL

Digital Library

[30]

Atshushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Proceedings of the 14th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA ’99, pages 132–146, New York, NY, USA, 1999. ACM. ISBN 1-58113-238-7. URL

Digital Library

[31]

JPF. JavaPathFinder. http://babelfish.arc.nasa.gov/trac/jpf/ .

[32]

James C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385–394, 1976. ISSN 0001-0782.

Digital Library

[33]

Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run your research: on the effectiveness of lightweight mechanization. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 285–296. ACM, 2012a. ISBN 978-1-4503-1083-3. URL

Digital Library

[34]

Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run your research: On the effectiveness of lightweight mechanization. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, pages 285–296, New York, NY, USA, 2012b. ACM. ISBN 978-1-4503-1083-3. URL

Digital Library

[35]

Casey Klein, Matthew Flatt, and Robert Bruce Findler. The racket virtual machine and randomized testing. Higher Order Symbol. Comput., 25(2-4):209–253, December 2012c. ISSN 1388-3690. URL

Digital Library

[36]

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Constraints as control. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’12, pages 151–164, New York, NY, USA, 2012. ACM. ISBN 978-1-4503-1083-3. URL

Digital Library

[37]

Daniel Kroening. CBMC. http://www.cprover.org/cbmc/ .

[38]

Nikolay Mateev, Keshav Pingali, Paul Stodghill, and Vladimir Kotlyar. Next-generation generic programming and its application to sparse matrix computations. In Proceedings of ICS’00, pages 88–99, 2000.

Digital Library

[39]

James McDonald and John Anton. SPECWARE - producing software correct by construction. Technical Report KES.U.01.3., 2001.

[40]

Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. Higher-order symbolic execution for contract verification and refutation. CoRR, abs/1507.04817, 2015. URL http://arxiv.org/abs/1507.04817 .

[41]

Tobias Nipkow and David von Oheimb. Java ℓi4ht is type-safe — definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 161–170. ACM Press, 1998.

[42]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg, 2002. ISBN 3-540-43376-7.

[43]

Martin Odersky. We got liftoff! The Dotty compiler for Scala bootstraps. http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-bootstraps.html, 2015.

[44]

Martin Odersky. Scaling DOT to Scala - soundness. http://scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html, 2016.

[45]

Martin Odersky and al. An overview of the Scala programming language. Technical Report IC/2004/64, EPFL, Lausanne, Switzerland, 2004.

[46]

Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 1st edition, 2002. ISBN 0262162091, 9780262162098.

Digital Library

[47]

Markus Püschel, José M. F. Moura, Jeremy Johnson, David Padua, Manuela Veloso, Bryan Singer, Jianxin Xiong, Franz Franchetti, Aca Gacic, Yevgen Voronenko, Kang Chen, Robert W. Johnson, and Nicholas Rizzolo. SPIRAL: Code generation for DSP transforms. Proceedings of the IEEE, special issue on “Program Generation, Optimization, and Adaptation”, 93(2):232– 275, 2005.

[48]

Michael Roberson and Chandrasekhar Boyapati. Efficient modular glass box software model checking. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’10, pages 4–21, New York, NY, USA, 2010. ACM. ISBN 978-1-4503-0203-6. URL

Digital Library

[49]

Michael Roberson, Melanie Harries, Paul T. Darga, and Chandrasekhar Boyapati. Efficient software model checking of soundness of type systems. In Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications, OOPSLA ’08, pages 493–504, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-215-3. URL

Digital Library

[50]

Burke Fetscher Robert Bruce Findler, Casey Klein and Matthias Felleisen. Redex: Practical Semantics Engineering, 2017. URL http://docs.racket-lang.org/redex/index.html .

[51]

Tiark Rompf and Nada Amin. From F to DOT: Type soundness proofs with definitional interpreters. Technical report, Purdue University and EPFL, 2016.

[52]

Eric L. Seidel, Ranjit Jhala, and Westley Weimer. Dynamic witnesses for static type errors. In 21st ACM SIGPLAN International Conference on Functional Programming, 2016. URL http://eric.seidel.io/pub/nanomaly-icfp16.pdf .

Digital Library

[53]

Koushik Sen, Swaroop Kalasapur, Tasneem G. Brutch, and Simon Gibbs. Jalangi: a selective record-replay and dynamic analysis framework for javascript. In Bertrand Meyer, Luciano Baresi, and Mira Mezini, editors, Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26, 2013, pages 488–498. ACM, 2013. URL

Digital Library

[54]

Koushik Sen, George C. Necula, Liang Gong, and Wontae Choi. Multise: multi-path symbolic execution using value summaries. In Elisabetta Di Nitto, Mark Harman, and Patrick Heymans, editors, Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, Bergamo, Italy, August 30 - September 4, 2015, pages 842–853. ACM, 2015. URL

Digital Library

[55]

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. In Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, ASPLOS XII, pages 404–415, New York, NY, USA, 2006. ACM. ISBN 1-59593-451-0. URL

Digital Library

[56]

Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. From program verification to program synthesis. In POPL, 2010.

Digital Library

[57]

Bernhard Steffen. Property-oriented expansion. In Radhia Cousot and David A. Schmidt, editors, Static Analysis, Third International Symposium, SAS’96, Aachen, Germany, September 24-26, 1996, Proceedings, volume 1145 of Lecture Notes in Computer Science, pages 22–41. Springer, 1996. ISBN 3-540-61739-6. URL

[58]

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

[59]

The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. URL http://coq.inria.fr .

[60]

Mads Tofte. Type inference for polymorphic references. Inf. Comput., 89(1):1–34, 1990a. URL

Digital Library

[61]

Mads Tofte. Type inference for polymorphic references. Inf. Comput., 89(1):1–34, September 1990b. ISSN 0890-5401. URL

Digital Library

[62]

Emina Torlak. The Rosette Guide. University of Washington, 2016. URL http://emina.github.io/rosette/doc/rosette-guide/index.html .

[63]

Emina Torlak and Rastislav Bodík. A lightweight symbolic virtual machine for solver-aided host languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, page 54, 2014. URL

Digital Library

[64]

Emina Torlak and Rastislav Bodik. 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, pages 530–541, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2784-8. URL

Digital Library

[65]

Emina Torlak, Mandana Vaziri, and Julian Dolby. MemSAT: Checking axiomatic specifications of memory models. In Programming Language Design and Implementation (PLDI’10), pages 341–350, 2010.

Digital Library

[66]

Martin T. Vechev, Eran Yahav, and David F. Bacon. Correctness-preserving derivation of concurrent garbage collection algorithms. In PLDI, pages 341–353, 2006.

Digital Library

[67]

A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38–94, November 1994. ISSN 0890-5401. URL

Digital Library

[68]

Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and understanding bugs in c compilers. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, pages 283–294, New York, NY, USA, 2011. ACM. ISBN 978-1-4503-0663-8. URL

Digital Library

[69]

Andreas Zeller. Yesterday, my program worked. today, it does not. why? In Oscar Nierstrasz and Michel Lemoine, editors, Software Engineering - ESEC/FSE’99, 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France, September 1999, Proceedings, volume 1687 of Lecture Notes in Computer Science, pages 253–267. Springer, 1999. ISBN 3-540-66538-2. URL

Cited By

Lu SBodík R(2023)Grisette: Symbolic Compilation as a Functional Programming LibraryProceedings of the ACM on Programming Languages10.1145/35712097:POPL(455-487)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571209
Chen YLiu JFeng YBodik RFalsafi BFerdman MLu SWenisch T(2022)Tree traversal synthesis using domain-specific symbolic compilationProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3503222.3507751(1030-1042)Online publication date: 28-Feb-2022
https://dl.acm.org/doi/10.1145/3503222.3507751
Porncharoenwase SNelson LWang XTorlak E(2022)A formal foundation for symbolic evaluation with mergingProceedings of the ACM on Programming Languages10.1145/34987096:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498709
Show More Cited By

Index Terms

Bonsai: synthesis-based reasoning for type systems
1. Software and its engineering

Recommendations

Type checking and typability in domain-free lambda calculi

This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Unifying type checking and property checking for low-level code
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, program-specific invariants that are difficult for traditional type ...

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 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Funding Sources

Intel
Mozilla
DARPA
Google
NSF

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
717
Total Downloads

Downloads (Last 12 months)126
Downloads (Last 6 weeks)21

Reflects downloads up to 05 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lu SBodík R(2023)Grisette: Symbolic Compilation as a Functional Programming LibraryProceedings of the ACM on Programming Languages10.1145/35712097:POPL(455-487)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571209
Chen YLiu JFeng YBodik RFalsafi BFerdman MLu SWenisch T(2022)Tree traversal synthesis using domain-specific symbolic compilationProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3503222.3507751(1030-1042)Online publication date: 28-Feb-2022
https://dl.acm.org/doi/10.1145/3503222.3507751
Porncharoenwase SNelson LWang XTorlak E(2022)A formal foundation for symbolic evaluation with mergingProceedings of the ACM on Programming Languages10.1145/34987096:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498709
Pearce D(2021)A Lightweight Formalism for Reference Lifetimes and Borrowing in RustACM Transactions on Programming Languages and Systems10.1145/344342043:1(1-73)Online publication date: 17-Apr-2021
https://dl.acm.org/doi/10.1145/3443420
Porncharoenwase SBornholt JTorlak E(2020)Fixing Code that Explodes Under Symbolic EvaluationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_3(44-67)Online publication date: 16-Jan-2020
https://dl.acm.org/doi/10.1007/978-3-030-39322-9_3
Orvalho PTerra-Neves MVentura MMartins RManquinho V(2019)Encodings for Enumeration-Based Program SynthesisPrinciples and Practice of Constraint Programming10.1007/978-3-030-30048-7_34(583-599)Online publication date: 30-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30048-7_34
Bornholt JTorlak E(2018)Finding code that explodes under symbolic evaluationProceedings of the ACM on Programming Languages10.1145/32765192:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276519

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents