Publications

The Essence of Program Semantics Visualizers: A Three-Axis Model
Josh Pollock, Grace Oh, Eunice Jun, Philip J. Guo, Zachary Tatlock
Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU) 2020
  paper  

A program semantics visualizer (PSV) helps illuminate a language’s semantics by explaining the runtime execution of programs. PSVs are often used in introductory programming (CS1) courses to help introduce a notional machine, an abstraction of the computer that executes the language. But what information should PSVs present to fully explain such notional machines?

In this paper we propose a three-axis model to assess the design of PSVs that visualize execution traces. PSVs should help users by clearly answering three questions: What is the machine’s configuration at each execution step? Why did an execution step take place? How did an execution step change the machine’s configuration? We demonstrate our model’s utility for assessing PSVs by explaining why, in actual classroom use, instructors have resorted to manually extending Python Tutor’s visualizations.

See also:

Towards Numerical Assistants
Pavel Panchekha, Zachary Tatlock
Numerical Software Verification (NSV) 2020
  paper   talk   slides   Herbie   FPBench  

The last few years have seen an explosion of work on tools that address numerical error in scientific, mathematical, and engineering software. The resulting tools can provide essential guidance to expert non-experts: scientists, mathematicians, and engineers for whom mathematical computation is essential but who may have little formal training in numerical methods. It is now time for these tools to move into practice.

Practitioners need a “numerical workbench” that not only succeeds as a research artifact but as a daily tool. We describe our experience adapting Herbie, a tool for numerical error repair, from a research prototype to a reliable workhorse for daily use. In particular, we focus on how we worked to increase user trust and use internal measurement to polish the tool. Looking more broadly, we show that community development and an investment in the generality of our tools, such as through the FPBench project, will better support users and strengthen our research community.


      @inproceedings{2016-nsv-fpbench,
        author    = {Pavel Panchekha and
                     Zachary Tatlock},
        title     = {Towards Numerical Assistants},
        booktitle = {Numerical Software Verification - 13th International Workshop, {NSV} 2020,
                     Los Angeles, CA, USA, July 20-21, 2020, [collocated with {CAV} 2020],
                     Revised Selected Papers},
        series    = {Lecture Notes in Computer Science},
      }

Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox,
Eva Darulova, Dan Grossman, Zachary Tatlock
Programming Language Design and Implementation (PLDI) 2020
paper   teaser   talk   slides   poster   code   project  


      @inproceedings{2020-pldi-szalinski-cad-eqsat,
        author    = {Chandrakana Nandi and
                     Max Willsey and
                     Adam Anderson and
                     James R. Wilcox and
                     Eva Darulova and
                     Dan Grossman and
                     Zachary Tatlock},
        editor    = {Alastair F. Donaldson and
                     Emina Torlak},
        title     = {Synthesizing Structured {CAD} Models with Equality Saturation and
                     Inverse Transformations},
        booktitle = {Proceedings of the 41st {ACM} {SIGPLAN} International Conference on
                     Programming Language Design and Implementation, {PLDI} 2020,
                     London, UK, June 15-20, 2020},
        pages     = {31--44},
        publisher = {{ACM}},
        year      = {2020},
        url       = {https://doi.org/10.1145/3385412.3386012},
        doi       = {10.1145/3385412.3386012},
      }

Carpentry Compiler
Chenming Wu, Haisen Zhao, Chandrakana Nandi,
Jeffrey I. Lipton, Zachary Tatlock, Adriana Schulz
ACM Transactions on Graphics (SIGGRAPH ASIA) 2019
  paper   appendix   teaser   slides   code   project  

Traditional manufacturing workflows strongly decouple design and fabrication phases. As a result, fabrication-related objectives such as manufacturing time and precision are difficult to optimize in the design space, and vice versa.

This paper presents HL-HELM, a high-level, domain-specific language for expressing abstract, parametric fabrication plans; it also introduces LL-HELM, a low-level language for expressing concrete fabrication plans that take into account the physical constraints of available manufacturing processes. We present a new compiler that supports the real-time, unoptimized translation of high-level, geometric fabrication operations into concrete, tool-specific fabrication instructions; this gives users immediate feedback on the physical feasibility of plans as they design them.

HELM offers novel optimizations to improve accuracy and reduce fabrication time as well as material costs. Optimized low-level plans can be interpreted as step-by-step instructions for users to actually fabricate a physical product. We provide a variety of example fabrication plans in the carpentry domain that are designed using our high-level language, show how the compiler translates and optimizes these plans to generate concrete low-level instructions, and present the final physical products fabricated in wood.

Press:


      @article{2019-siga-carpentry-compiler,
        author    = {Chenming Wu and
                     Haisen Zhao and
                     Chandrakana Nandi and
                     Jeffrey I. Lipton and
                     Zachary Tatlock and
                     Adriana Schulz},
        title     = {Carpentry compiler},
        journal   = {{ACM} Transactions on Graphics},
        volume    = {38},
        number    = {6},
        pages     = {195:1--195:14},
        year      = {2019},
        url       = {https://doi.org/10.1145/3355089.3356518},
        doi       = {10.1145/3355089.3356518},
      }

Modular Verification of Web Page Layout
Pavel Panchekha, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2019
paper   talk   slides   code   project  


      @article{2019-oopsla-troika-modular-layout-verification,
        author    = {Pavel Panchekha and
                     Michael D. Ernst and
                     Zachary Tatlock and
                     Shoaib Kamil},
        title     = {Modular Verification of Web Page Layout},
        journal   = {Proceedings of the {ACM} on Programming Languages},
        volume    = {3},
        number    = {{OOPSLA}},
        pages     = {151:1--151:26},
        year      = {2019},
        url       = {https://doi.org/10.1145/3360577},
        doi       = {10.1145/3360577},
      }

Theia: Automatically Generating Correct Program State Visualizations
Josh Pollock, Jared Roesch, Doug Woos, Zachary Tatlock
ACM SIGPLAN Symposium on SPLASH-E 2019
  paper   code  

Program state visualizations (PSVs) help programmers understand hidden program state like objects, references, and closures. Unfortunately, existing PSV tools do not support custom language semantics, which educators often use to introduce programming languages gradually. They also fail to visualize key pieces of program state, which can lead to incorrect and confusing visualizations.

Theia, a generic PSV framework, uses formal abstract machine definitions to produce complete, continuous, and consistent (CCC) PSVs.

To produce CCC visualizations with Theia, an educator only needs to specify an abstract machine and optionally customize the resulting web page, allowing her to visualize custom language semantics without developing a language specific tool.

See also:

QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
Foundations and Trends in Programming Languages (FTPL) 2019
paper   errata   project  


      @article{2019-ftpl-qed-at-large,
        author    = {Talia Ringer and
                     Karl Palmskog and
                     Ilya Sergey and
                     Milos Gligoric and
                     Zachary Tatlock},
        title     = {{QED} at Large: {A} Survey of Engineering of Formally Verified Software},
        journal   = {Foundations and Trends in Programming Languages},
        volume    = {5},
        number    = {2-3},
        pages     = {102--281},
        year      = {2019},
        url       = {https://doi.org/10.1561/2500000045},
        doi       = {10.1561/2500000045},
      }

Toward Multi-Precision, Multi-Format Numerics
David Thien, Bill Zorn, Pavel Panchekha, Zachary Tatlock
Software Correctness for HPC Applications (CORRECTNESS) 2019
paper   slides   FPBench   Titanic   Herbie  


      @inproceedings{2019-correctness-mpmf,
        author    = {David Thien and
                     Bill Zorn and
                     Pavel Panchekha and
                     Zachary Tatlock},
        editor    = {Ignacio Laguna and
                     Cindy Rubio{-}Gonz{\'{a}}lez},
        title     = {Toward Multi-Precision, Multi-Format Numerics},
        booktitle = {2019 {IEEE/ACM} 3rd International Workshop on
                     Software Correctness for {HPC} Applications (Correctness),
                     Denver, CO, {USA},
                     November 18, 2019},
        pages     = {19--26},
        publisher = {{IEEE}},
        year      = {2019},
        url       = {https://doi.org/10.1109/Correctness49594.2019.00008},
        doi       = {10.1109/Correctness49594.2019.00008},
      }

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
Computer-Aided Verification (CAV) 2019
paper   slides   code   project  


      @inproceedings{2019-cav-icing-verified-fastmath,
        author    = {Heiko Becker and
                     Eva Darulova and
                     Magnus O. Myreen and
                     Zachary Tatlock},
        editor    = {Isil Dillig and
                     Serdar Tasiran},
        title     = {Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler},
        booktitle = {Computer Aided Verification - 31st International Conference,
                     {CAV} 2019,
                     New York City, NY, USA,
                     July 15-18, 2019,
                     Proceedings, Part {II}},
        series    = {Lecture Notes in Computer Science},
        volume    = {11562},
        pages     = {155--173},
        publisher = {Springer},
        year      = {2019},
        url       = {https://doi.org/10.1007/978-3-030-25543-5\_10},
        doi       = {10.1007/978-3-030-25543-5\_10},
      }

Teaching Rigorous Distributed Systems With Efficient Model Checking
Ellis Michael, Doug Woos, Thomas E. Anderson, Michael D. Ernst, Zachary Tatlock
European Conference on Computer Systems (EuroSys) 2019
paper   talk   slides   code  


      @inproceedings{2019-eurosys-dslabs,
        author    = {Ellis Michael and
                     Doug Woos and
                     Thomas E. Anderson and
                     Michael D. Ernst and
                     Zachary Tatlock},
        editor    = {George Candea and
                     Robbert van Renesse and
                     Christof Fetzer},
        title     = {Teaching Rigorous Distributed Systems
                     with Efficient Model Checking},
        booktitle = {Proceedings of the Fourteenth EuroSys Conference 2019,
                     Dresden, Germany,
                     March 25-28, 2019},
        pages     = {32:1--32:15},
        publisher = {{ACM}},
        year      = {2019},
        url       = {https://doi.org/10.1145/3302424.3303947},
        doi       = {10.1145/3302424.3303947},
      }

Sinking Point: Dynamic Precision Tracking for Floating-Point
Bill Zorn, Dan Grossman, Zachary Tatlock
Conference for Next Generation Arithmetic (CoNGA) 2019
  paper   talk   slides   code   project  

We present sinking-point, a floating-point-like number system that tracks precision dynamically though computations. With existing floating-point number systems, such as the venerable IEEE 754 standard, numerical results do not inherently contain any information about their precision or accuracy; to determine if a result is numerically accurate, a separate analysis must be performed. By contrast, sinking-point records the precision of each intermediate value and result computed, so highly imprecise results can be identified immediately. Compared to IEEE 754 floating-point, sinking-point’s representation requires only a few additional bits of storage, and computations require only a few additional bitwise operations. Sinking-point is fully generalizable, and can be extended to provide dynamic error tracking for nearly any digital number system, including posits.


      @inproceedings{2019-conga-sinking-point,
        author    = {Bill Zorn and
                     Dan Grossman and
                     Zachary Tatlock},
        title     = {Sinking Point: Dynamic Precision Tracking for Floating-Point},
        year      = {2019},
        isbn      = {9781450371391},
        publisher = {Association for Computing Machinery},
        address   = {New York, NY, USA},
        url       = {https://doi.org/10.1145/3316279.3316283},
        doi       = {10.1145/3316279.3316283},
        booktitle = {Proceedings of the Conference for Next Generation Arithmetic 2019},
        articleno = {4},
        numpages  = {8},
        keywords  = {Floating point, numerical analysis},
        location  = {Singapore, Singapore},
        series    = {CoNGA'19}
      }

Functional Programming for Compiling and Decompiling Computer-aided Design
Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau,
Dan Grossman, Zachary Tatlock
International Conference on Functional Programming (ICFP) 2018
paper   talk   slides   poster   code   project   I Am CSE  


      @article{2018-icfp-reincarnate-cad-decompiler,
        author    = {Chandrakana Nandi and
                     James R. Wilcox and
                     Pavel Panchekha and
                     Taylor Blau and
                     Dan Grossman and
                     Zachary Tatlock},
        title     = {Functional Programming for Compiling and Decompiling Computer-aided Design},
        journal   = {Proceedings of the {ACM} on Programming Languages},
        volume    = {2},
        number    = {{ICFP}},
        pages     = {99:1--99:31},
        year      = {2018},
        url       = {https://doi.org/10.1145/3236794},
        doi       = {10.1145/3236794},
      }

Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock
Formal Methods (FM) 2018
short paper   slides   Daisy   Herbie   FPBench  


      @inproceedings{2018-fm-combining-fp-tools,
        author    = {Heiko Becker and
                     Pavel Panchekha and
                     Eva Darulova and
                     Zachary Tatlock},
        editor    = {Klaus Havelund and
                     Jan Peleska and
                     Bill Roscoe and
                     Erik P. de Vink},
        title     = {Combining Tools for Optimization and Analysis of Floating-Point Computations},
        booktitle = {Formal Methods - 22nd International Symposium, {FM} 2018,
                     Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK,
                     July 15-17, 2018, Proceedings},
        series    = {Lecture Notes in Computer Science},
        volume    = {10951},
        pages     = {355--363},
        publisher = {Springer},
        year      = {2018},
        url       = {https://doi.org/10.1007/978-3-319-95582-7\_21},
        doi       = {10.1007/978-3-319-95582-7\_21},
      }

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB
Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen
Interactive Theorem Proving (ITP) 2018
short paper   slides   CakeML   Oeuf  


      @inproceedings{2018-itp-binary-code-extraction,
        author    = {Ramana Kumar and
                     Eric Mullen and
                     Zachary Tatlock and
                     Magnus O. Myreen},
        editor    = {Jeremy Avigad and
                     Assia Mahboubi},
        title     = {Software Verification with ITPs Should Use Binary Code Extraction
                     to Reduce the {TCB} - (Short Paper)},
        booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP} 2018,
                     Held as Part of the Federated Logic Conference, FloC 2018,
                     Oxford, UK, July 9-12, 2018, Proceedings},
        series    = {Lecture Notes in Computer Science},
        volume    = {10895},
        pages     = {362--369},
        publisher = {Springer},
        year      = {2018},
        url       = {https://doi.org/10.1007/978-3-319-94821-8\_21},
        doi       = {10.1007/978-3-319-94821-8\_21},
      }

Verifying that Web Pages have Accessible Layout
Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Programming Language Design and Implementation (PLDI) 2018
paper   talk   slides   code   project  


      @inproceedings{2018-pldi-vizassert-web-layout,
        author    = {Pavel Panchekha and
                     Adam T. Geller and
                     Michael D. Ernst and
                     Zachary Tatlock and
                     Shoaib Kamil},
        editor    = {Jeffrey S. Foster and
                     Dan Grossman},
        title     = {Verifying that Web Pages have Accessible Layout},
        booktitle = {Proceedings of the 39th {ACM} {SIGPLAN} Conference on
                     Programming Language Design and Implementation, {PLDI} 2018,
                     Philadelphia, PA, USA,
                     June 18-22, 2018},
        pages     = {1--14},
        publisher = {{ACM}},
        year      = {2018},
        url       = {https://doi.org/10.1145/3192366.3192407},
        doi       = {10.1145/3192366.3192407},
      }

Finding Root Causes of Floating Point Error
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
Programming Language Design and Implementation (PLDI) 2018
paper   talk   slides   code   project  


      @inproceedings{2018-pldi-herbgrind-fp-error,
        author    = {Alex Sanchez{-}Stern and
                     Pavel Panchekha and
                     Sorin Lerner and
                     Zachary Tatlock},
        editor    = {Jeffrey S. Foster and
                     Dan Grossman},
        title     = {Finding root causes of floating point error},
        booktitle = {Proceedings of the 39th {ACM} {SIGPLAN} Conference on
                     Programming Language Design and Implementation, {PLDI} 2018,
                     Philadelphia, PA, USA,
                     June 18-22, 2018},
        pages     = {256--269},
        publisher = {{ACM}},
        year      = {2018},
        url       = {https://doi.org/10.1145/3192366.3192411},
        doi       = {10.1145/3192366.3192411},
      }

Relay: a New IR for Machine Learning Frameworks
Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame,
Tianqi Chen, Zachary Tatlock
Machine Learning and Programming Languages (MAPL) 2018
paper   slides   code   project  


      @inproceedings{2018-mapl-relay-ir,
        author    = {Jared Roesch and
                     Steven Lyubomirsky and
                     Logan Weber and
                     Josh Pollock and
                     Marisa Kirisame and
                     Tianqi Chen and
                     Zachary Tatlock},
        editor    = {Justin Gottschlich and
                     Alvin Cheung},
        title     = {Relay: a New {IR} for Machine Learning Frameworks},
        booktitle = {Proceedings of the 2nd {ACM} {SIGPLAN} International Workshop on
                     Machine Learning and Programming Languages, MAPL@PLDI 2018,
                     Philadelphia, PA, USA,
                     June 18-22, 2018},
        pages     = {58--68},
        publisher = {{ACM}},
        year      = {2018},
        url       = {https://doi.org/10.1145/3211346.3211348},
        doi       = {10.1145/3211346.3211348},
      }

Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, Zachary Tatlock
Principles of Programming Languages (POPL) 2018
paper   talk   slides   code   project  


      @article{2018-popl-disel,
        author    = {Ilya Sergey and
                     James R. Wilcox and
                     Zachary Tatlock},
        title     = {Programming and Proving with Distributed Protocols},
        journal   = {Proceedings of the {ACM} on Programming Languages},
        volume    = {2},
        number    = {{POPL}},
        pages     = {28:1--28:30},
        year      = {2018},
        url       = {https://doi.org/10.1145/3158116},
        doi       = {10.1145/3158116},
      }

Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman
Certified Programs and Proofs (CPP) 2018
paper   slides   code   project  


      @inproceedings{2018-cpp-oeuf-coq-compiler,
        author    = {Eric Mullen and
                     Stuart Pernsteiner and
                     James R. Wilcox and
                     Zachary Tatlock and
                     Dan Grossman},
        editor    = {June Andronick and
                     Amy P. Felty},
        title     = {{\OE}uf: Minimizing the Coq Extraction {TCB}},
        booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
                     Certified Programs and Proofs, {CPP} 2018,
                     Los Angeles, CA, USA,
                     January 8-9, 2018},
        pages     = {172--185},
        publisher = {{ACM}},
        year      = {2018},
        url       = {https://doi.org/10.1145/3167089},
        doi       = {10.1145/3167089},
      }

Automatic Formal Verification for EPICS
Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric,
Stuart Pernsteiner, Zachary Tatlock, Emina Torlak
International Conference on Accelerator and Large Experimental Control Systems (ICALEPCS) 2017
  paper   talk   slides   code   project   publisher  

We built an EPICS-based radiation therapy machine control system, and are using it to treat patients at our hospital. To help ensure safety, we use a restricted subset of EPICS constructs and programming techniques, and developed several new automated formal verification tools for them. The Symbolic Evaluator checks properties of EPICS database programs (applications), using symbolic evaluation and satisfiability checking. It found serious errors in our control program that were missed by reviews and testing. Other tools are based on a formal semantics for database records, derived from EPICS documentation and expressed in the specification language of an automated theorem prover. The Verified Interpreter is a re-implementation of the parts of the database engine we use, which is proved correct against the formal semantics. We used it to check those parts of EPICS core by differential testing. It found no significant errors (differences between EPICS behavior and the formal semantics). A Verified Compiler is in development. It will compile a database to a standalone program that does not use EPICS core, where the machine code is verified to conform to the formal semantics.


      @inproceedings{2017-icalepcs-epics-verification,
        author       = {Jonathan Jacky and
                        Stefani Banerian and
                        Michael D. Ernst and
                        Calvin Loncaric and
                        Stuart Pernsteiner and
                        Zachary Tatlock and
                        Emina Torlak},
        title        = {{A}utomatic {F}ormal {V}erification for {EPICS}},
        booktitle    = {Proc. of International Conference on Accelerator and Large Experimental Control Systems (ICALEPCS'17),
                        Barcelona, Spain, 8-13 October 2017},
        pages        = {285--291},
        paper        = {TUDPL02},
        language     = {english},
        keywords     = {ion, EPICS, controls, database, operation},
        venue        = {Barcelona, Spain},
        series       = {International Conference on Accelerator and Large Experimental Control Systems},
        number       = {16},
        publisher    = {JACoW},
        address      = {Geneva, Switzerland},
        month        = {January},
        year         = {2018},
        isbn         = {978-3-95450-193-9},
        doi          = {https://doi.org/10.18429/JACoW-ICALEPCS2017-TUDPL02},
        url          = {http://jacow.org/icalepcs2017/papers/tudpl02.pdf},
        note         = {https://doi.org/10.18429/JACoW-ICALEPCS2017-TUDPL02},
      }

SpaceSearch: A Library for Building and Verifying Solver-aided Tools
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule,
Emina Torlak, Michael D. Ernst, Zachary Tatlock
International Conference on Functional Programming (ICFP) 2017
paper   talk   slides   code   project  


      @article{2017-icfp-spacesearch-verifying-solver-aided-tools,
        author    = {Konstantin Weitz and
                     Steven Lyubomirsky and
                     Stefan Heule and
                     Emina Torlak and
                     Michael D. Ernst and
                     Zachary Tatlock},
        title     = {SpaceSearch: A Library for Building and Verifying Solver-aided Tools},
        journal   = {Proceedings of the {ACM} on Programming Languages},
        volume    = {1},
        number    = {{ICFP}},
        pages     = {25:1--25:28},
        year      = {2017},
        url       = {https://doi.org/10.1145/3110269},
        doi       = {10.1145/3110269},
      }

Programming Language Tools and Techniques for 3D Printing
Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock
Summit oN Advances in Programming Languages (SNAPL) 2017
paper   slides   project  


      @inproceedings{2017-snapl-incarnate-pl-for-3d-printing,
        author    = {Chandrakana Nandi and
                     Anat Caspi and
                     Dan Grossman and
                     Zachary Tatlock},
        editor    = {Benjamin S. Lerner and
                     Rastislav Bod{\'{\i}}k and
                     Shriram Krishnamurthi},
        title     = {Programming Language Tools and Techniques for 3D Printing},
        booktitle = {2nd Summit on Advances in Programming Languages, {SNAPL} 2017,
                     May 7-10, 2017, Asilomar, CA, {USA}},
        series    = {LIPIcs},
        volume    = {71},
        pages     = {10:1--10:12},
        publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
        year      = {2017},
        url       = {https://doi.org/10.4230/LIPIcs.SNAPL.2017.10},
        doi       = {10.4230/LIPIcs.SNAPL.2017.10},
      }

Programming Language Abstractions for Modularly Verified Distributed Systems
James R. Wilcox, Ilya Sergey, Zachary Tatlock
Summit oN Advances in Programming Languages (SNAPL) 2017
paper   slides   project  


      @inproceedings{2017-snapl-disel-pl-for-distributed-systems,
        author    = {James R. Wilcox and
                     Ilya Sergey and
                     Zachary Tatlock},
        editor    = {Benjamin S. Lerner and
                     Rastislav Bod{\'{\i}}k and
                     Shriram Krishnamurthi},
        title     = {Programming Language Abstractions for
                     Modularly Verified Distributed Systems},
        booktitle = {2nd Summit on Advances in Programming Languages, {SNAPL} 2017,
                     May 7-10, 2017, Asilomar, CA, {USA}},
        series    = {LIPIcs},
        volume    = {71},
        pages     = {19:1--19:12},
        publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
        year      = {2017},
        url       = {https://doi.org/10.4230/LIPIcs.SNAPL.2017.19},
        doi       = {10.4230/LIPIcs.SNAPL.2017.19},
      }

Verification of Implementations of Distributed Systems Under Churn
Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, Karl Palmskog
Workshop on Coq for Programming Languages (CoqPL) 2017
paper   slides   code   project  

Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver
Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2016
paper   talk   slides   code   project  


      @inproceedings{2016-oopsla-bagpipe-scalable-bgp-verification-smt,
        author    = {Konstantin Weitz and
                     Doug Woos and
                     Emina Torlak and
                     Michael D. Ernst and
                     Arvind Krishnamurthy and
                     Zachary Tatlock},
        editor    = {Eelco Visser and
                     Yannis Smaragdakis},
        title     = {Scalable Verification of Border Gateway Protocol Configurations
                     with an {SMT} Solver},
        booktitle = {Proceedings of the 2016 {ACM} {SIGPLAN} International Conference on
                     Object-Oriented Programming, Systems, Languages, and Applications,
                     {OOPSLA} 2016, part of {SPLASH} 2016,
                     Amsterdam, The Netherlands,
                     October 30 - November 4, 2016},
        pages     = {765--780},
        publisher = {{ACM}},
        year      = {2016},
        url       = {https://doi.org/10.1145/2983990.2984012},
        doi       = {10.1145/2983990.2984012},
      }

Formal Semantics and Automated Verification for the Border Gateway Protocol
Konstantin Weitz, Doug Woos, Emina Torlak,
Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL) 2016
  paper   slides   code   project  

We present the first mechanized formal semantics of BGP (implemented in the Coq proof assistant) that models all required features of the BGP specification RFC-4271 modulo low-level details. We demonstrate our semantic’s correctness and usefulness by: 1) extending and formalizing the pen-and-paper proof by Gao & Rexford on the convergence of BGP, revealing necessary extensions to their original configuration guidelines; 2) building the Bagpipe tool which automatically checks that BGP configurations adhere to given policy specifications, revealing 19 apparent errors in three ASes with over 240,000 lines of BGP configuration; and 3) testing the BGP simulator C-BGP, revealing one bug.


      @inproceedings{2016-netpl-bagpipe-bgp-verification,
        author    = {Konstantin Weitz and
                     Doug Woos and
                     Emina Torlak and
                     Michael D. Ernst and
                     Arvind Krishnamurthy and
                     Zachary Tatlock},
        title     = {Formal Semantics and Automated Verification for the Border Gateway Protocol},
        year      = {2016},
        publisher = {Association for Computing Machinery},
        address   = {New York, NY, USA},
        url       = {https://conferences.sigcomm.org/sigcomm/2016/netpl.php},
        booktitle = {Proceedings of the ACM SIGCOMM 2016 Workshop on Networking and Programming Languages},
        keywords  = {network verification, network simulation, control plane modelling},
        location  = {Florianopolis, Brazil},
        series    = {NetPL'16}
      }

Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers
Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock,
Xi Wang, Michael D. Ernst, Jonathan Jacky
Computer-Aided Verification (CAV) 2016
paper   slides   code   project   I Am CSE  


      @inproceedings{2016-cav-neutrons-radiotherapy-safety,
        author    = {Stuart Pernsteiner and
                     Calvin Loncaric and
                     Emina Torlak and
                     Zachary Tatlock and
                     Xi Wang and
                     Michael D. Ernst and
                     Jonathan Jacky},
        editor    = {Swarat Chaudhuri and
                     Azadeh Farzan},
        title     = {Investigating Safety of a Radiotherapy Machine Using System Models
                     with Pluggable Checkers},
        booktitle = {Computer Aided Verification - 28th International Conference,
                     {CAV} 2016,
                     Toronto, ON, Canada,
                     July 17-23, 2016,
                     Proceedings, Part {II}},
        series    = {Lecture Notes in Computer Science},
        volume    = {9780},
        pages     = {23--41},
        publisher = {Springer},
        year      = {2016},
        url       = {https://doi.org/10.1007/978-3-319-41540-6\_2},
        doi       = {10.1007/978-3-319-41540-6\_2},
      }

Toward a Standard Benchmark Format and Suite for Floating-Point Analysis
Nasrine Damouche, Matthieu Martel, Pavel Panchekha,
Chen Qiu, Alex Sanchez-Stern, Zachary Tatlock
Numerical Software Verification (NSV) 2016
paper   talk   slides   code   project  


      @inproceedings{2016-nsv-fpbench,
        author    = {Nasrine Damouche and
                     Matthieu Martel and
                     Pavel Panchekha and
                     Chen Qiu and
                     Alex Sanchez{-}Stern and
                     Zachary Tatlock},
        editor    = {Sergiy Bogomolov and
                     Matthieu Martel and
                     Pavithra Prabhakar},
        title     = {Toward a Standard Benchmark Format and Suite for Floating-Point Analysis},
        booktitle = {Numerical Software Verification - 9th International Workshop, {NSV} 2016,
                     Toronto, ON, Canada, July 17-18, 2016, [collocated with {CAV} 2016],
                     Revised Selected Papers},
        series    = {Lecture Notes in Computer Science},
        volume    = {10152},
        pages     = {63--77},
        year      = {2016},
        url       = {https://doi.org/10.1007/978-3-319-54292-8\_6},
        doi       = {10.1007/978-3-319-54292-8\_6},
      }

Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman
Programming Language Design and Implementation (PLDI) 2016
paper   talk   code   project  


      @inproceedings{2016-pldi-peek-verified-peepholes-compcert,
        author    = {Eric Mullen and
                     Daryl Zuniga and
                     Zachary Tatlock and
                     Dan Grossman},
        editor    = {Chandra Krintz and
                     Emery Berger},
        title     = {Verified peephole optimizations for CompCert},
        booktitle = {Proceedings of the 37th {ACM} {SIGPLAN} Conference on
                     Programming Language Design and Implementation, {PLDI} 2016,
                     Santa Barbara, CA,
                     USA, June 13-17, 2016},
        pages     = {448--461},
        publisher = {{ACM}},
        year      = {2016},
        url       = {https://doi.org/10.1145/2908080.2908109},
        doi       = {10.1145/2908080.2908109},
      }

Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson
Certified Programs and Proofs (CPP) 2016
paper   slides   code   Verdi   Proof Engineering  


      @inproceedings{2016-cpp-verdi-raft-proof-engineering,
        author    = {Doug Woos and
                     James R. Wilcox and
                     Steve Anton and
                     Zachary Tatlock and
                     Michael D. Ernst and
                     Thomas E. Anderson},
        editor    = {Jeremy Avigad and
                     Adam Chlipala},
        title     = {Planning for Change in a Formal Verification
                     of the Raft Consensus Protocol},
        booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on
                     Certified Programs and Proofs, {CPP} 2016,
                     Saint Petersburg, FL, USA,
                     January 20-22, 2016},
        pages     = {154--165},
        publisher = {{ACM}},
        year      = {2016},
        url       = {https://doi.org/10.1145/2854065.2854081},
        doi       = {10.1145/2854065.2854081},
      }

Automatically Improving Accuracy for Floating Point Expressions
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock
Programming Language Design and Implementation (PLDI) 2015
paper   teaser   talk   slides   code   project  
Distinguished Paper Award


      @inproceedings{2015-pldi-herbie-floating-point-accuracy,
        author    = {Pavel Panchekha and
                     Alex Sanchez{-}Stern and
                     James R. Wilcox and
                     Zachary Tatlock},
        editor    = {David Grove and
                     Steve Blackburn},
        title     = {Automatically improving accuracy for floating point expressions},
        booktitle = {Proceedings of the 36th {ACM} {SIGPLAN} Conference on
                     Programming Language Design and Implementation,
                     Portland, OR, USA,
                     June 15-17, 2015},
        pages     = {1--11},
        publisher = {{ACM}},
        year      = {2015},
        url       = {https://doi.org/10.1145/2737924.2737959},
        doi       = {10.1145/2737924.2737959},
      }

Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock,
Xi Wang, Michael D. Ernst, Thomas E. Anderson
Programming Language Design and Implementation (PLDI) 2015
paper   teaser   slides   poster   code   project  


      @inproceedings{2015-pldi-verdi-verifying-distributed-systems,
        author    = {James R. Wilcox and
                     Doug Woos and
                     Pavel Panchekha and
                     Zachary Tatlock and
                     Xi Wang and
                     Michael D. Ernst and
                     Thomas E. Anderson},
        editor    = {David Grove and
                     Steve Blackburn},
        title     = {Verdi: a Framework for Implementing and Formally Verifying Distributed Systems},
        booktitle = {Proceedings of the 36th {ACM} {SIGPLAN} Conference on
                     Programming Language Design and Implementation,
                     Portland, OR, USA,
                     June 15-17, 2015},
        pages     = {357--368},
        publisher = {{ACM}},
        year      = {2015},
        url       = {https://doi.org/10.1145/2737924.2737958},
        doi       = {10.1145/2737924.2737958},
      }

Toward a Dependability Case Language and Workflow for a Radiation Therapy System
Michael D. Ernst, Dan Grossman, Jonathan Jacky, Calvin Loncaric,
Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang
Summit oN Advances in Programming Languages (SNAPL) 2015
paper   slides   project   I Am CSE  


      @inproceedings{2015-snapl-neutrons-radiotherapy-safety,
        author    = {Michael D. Ernst and
                     Dan Grossman and
                     Jonathan Jacky and
                     Calvin Loncaric and
                     Stuart Pernsteiner and
                     Zachary Tatlock and
                     Emina Torlak and
                     Xi Wang},
        editor    = {Thomas Ball and
                     Rastislav Bod{\'{\i}}k and
                     Shriram Krishnamurthi and
                     Benjamin S. Lerner and
                     Greg Morrisett},
        title     = {Toward a Dependability Case Language and Workflow
                     for a Radiation Therapy System},
        booktitle = {1st Summit on Advances in Programming Languages, {SNAPL} 2015,
                     May 3-6, 2015,
                     Asilomar, California, {USA}},
        series    = {LIPIcs},
        volume    = {32},
        pages     = {103--112},
        publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
        year      = {2015},
        url       = {https://doi.org/10.4230/LIPIcs.SNAPL.2015.103},
        doi       = {10.4230/LIPIcs.SNAPL.2015.103},
      }

RoboFlow: A Flow-based Visual Programming Language for Mobile Manipulation Tasks
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
International Conference on Robotics and Automation (ICRA) 2015
paper   teaser   web GUI   code   project  


      @inproceedings{2015-icra-roboflow-visual-robot-programming-language,
        author    = {Sonya Alexandrova and
                     Zachary Tatlock and
                     Maya Cakmak},
        title     = {RoboFlow: {A} Flow-based Visual Programming Language
                     for Mobile Manipulation Tasks},
        booktitle = {{IEEE} International Conference on Robotics and Automation, {ICRA}
                     2015, Seattle, WA, USA,
                     26-30 May, 2015},
        pages     = {5537--5544},
        publisher = {{IEEE}},
        year      = {2015},
        url       = {https://doi.org/10.1109/ICRA.2015.7139973},
        doi       = {10.1109/ICRA.2015.7139973},
      }

Visual Robot Programming for Generalizable Mobile Manipulation Tasks (Extended Abstract)
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
Human Robot Interaction (HRI) 2015
paper   teaser   web GUI   code   project  


      @inproceedings{2015-hri-roboflow-visual-robot-programming-language,
        author    = {Sonya Alexandrova and
                     Zachary Tatlock and
                     Maya Cakmak},
        editor    = {Julie A. Adams and
                     William D. Smart and
                     Bilge Mutlu and
                     Leila Takayama},
        title     = {Visual Robot Programming for Generalizable Mobile Manipulation Tasks},
        booktitle = {Proceedings of the Tenth Annual {ACM/IEEE} International Conference on
                     Human-Robot Interaction, {HRI} 2015 Extended Abstracts,
                     Portland, OR, USA,
                     March 02 - 05, 2015},
        pages     = {163--164},
        publisher = {{ACM}},
        year      = {2015},
        url       = {https://doi.org/10.1145/2701973.2702052},
        doi       = {10.1145/2701973.2702052},
      }

Peek: A Formally Verified Peephole Optimization Framework for x86
Eric Mullen, Zachary Tatlock, Dan Grossman
Workshop on Coq for Programming Languages (CoqPL) 2015
paper   slides   code   project  

Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
Operating Systems Design and Implementation (OSDI) 2014
paper   talk   slides   code   project  


      @inproceedings{bib-2014-osdi-jitk-verified-bpf,
        author    = {Xi Wang and
                     David Lazar and
                     Nickolai Zeldovich and
                     Adam Chlipala and
                     Zachary Tatlock},
        editor    = {Jason Flinn and
                     Hank Levy},
        title     = {Jitk: {A} Trustworthy In-Kernel Interpreter Infrastructure},
        booktitle = {11th {USENIX} Symposium on Operating Systems Design and Implementation,
                     {OSDI} '14,
                     Broomfield, CO, {USA},
                     October 6-8, 2014},
        pages     = {33--47},
        publisher = {{USENIX} Association},
        year      = {2014},
        url       = {https://www.usenix.org/conference/osdi14/technical-sessions/presentation/wang\_xi},
      }

Automating Formal Proofs for Reactive Systems
Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation (PLDI) 2014
paper   talk   slides   code   project  


      @inproceedings{2014-pldi-reflex-reactive-systems-coq,
        author    = {Daniel Ricketts and
                     Valentin Robert and
                     Dongseok Jang and
                     Zachary Tatlock and
                     Sorin Lerner},
        editor    = {Michael F. P. O'Boyle and
                     Keshav Pingali},
        title     = {Automating Formal Proofs for Reactive Systems},
        booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
                     {PLDI} '14,
                     Edinburgh, United Kingdom -
                     June 09 - 11, 2014},
        pages     = {452--462},
        publisher = {{ACM}},
        year      = {2014},
        url       = {https://doi.org/10.1145/2594291.2594338},
        doi       = {10.1145/2594291.2594338},
      }

SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks
Dongseok Jang, Zachary Tatlock, Sorin Lerner
Network and Distributed System Security (NDSS) 2014
paper   slides   project  


      @inproceedings{2014-ndss-safe-dispatch-vtable-hijacking-defense,
        author    = {Dongseok Jang and
                     Zachary Tatlock and
                     Sorin Lerner},
        title     = {SafeDispatch: Securing {C++} Virtual Calls from Memory Corruption
                     Attacks},
        booktitle = {21st Annual Network and Distributed System Security Symposium,
                     {NDSS} 2014,
                     San Diego, California, {USA},
                     February 23-26, 2014},
        publisher = {The Internet Society},
        year      = {2014},
        url       = {https://www.ndss-symposium.org/ndss2014/safedispatch-securing-c-virtual-calls-memory-corruption-attacks},
      }

Establishing Browser Security Guarantees through Formal Shim Verification
Dongseok Jang, Zachary Tatlock, Sorin Lerner
USENIX Security Symposium 2012
paper   extended   talk   slides   poster   code   project  


      @inproceedings{2012-usenix-security-quark-formal-shim-verifiction-web-browser,
        author    = {Dongseok Jang and
                     Zachary Tatlock and
                     Sorin Lerner},
        editor    = {Tadayoshi Kohno},
        title     = {Establishing Browser Security Guarantees through Formal Shim Verification},
        booktitle = {Proceedings of the 21th {USENIX} Security Symposium,
                     Bellevue, WA,
                     {USA}, August 8-10, 2012},
        pages     = {113--128},
        publisher = {{USENIX} Association},
        year      = {2012},
        url       = {https://www.usenix.org/conference/usenixsecurity12/technical-sessions/presentation/jang},
      }

Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Logical Methods in Computer Science (LMCS) 2011
paper   project  


      @article{2011-lmcs-equality-saturation-optimizations-egraphs,
        author    = {Ross Tate and
                     Michael Stepp and
                     Zachary Tatlock and
                     Sorin Lerner},
        title     = {Equality Saturation: {A} New Approach to Optimization},
        journal   = {Logical Methods in Computer Science},
        volume    = {7},
        number    = {1},
        year      = {2011},
        url       = {https://doi.org/10.2168/LMCS-7(1:10)2011},
        doi       = {10.2168/LMCS-7(1:10)2011},
      }

Bringing Extensibility to Verified Compilers
Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation (PLDI) 2010
paper   slides   project  


      @inproceedings{2010-pldi-xcert-extensible-verified-compilers,
        author    = {Zachary Tatlock and
                     Sorin Lerner},
        editor    = {Benjamin G. Zorn and
                     Alexander Aiken},
        title     = {Bringing Extensibility to Verified Compilers},
        booktitle = {Proceedings of the 2010 {ACM} {SIGPLAN} Conference on
                     Programming Language Design and Implementation,
                     {PLDI} 2010,
                     Toronto, Ontario, Canada,
                     June 5-10, 2010},
        pages     = {111--121},
        publisher = {{ACM}},
        year      = {2010},
        url       = {https://doi.org/10.1145/1806596.1806611},
        doi       = {10.1145/1806596.1806611},
      }

Proving Optimizations Correct using Parameterized Program Equivalence
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation (PLDI) 2009
paper   talk   slides   code   project  


      @inproceedings{2009-pldi-pec-compiler-optimization-verification,
        author    = {Sudipta Kundu and
                     Zachary Tatlock and
                     Sorin Lerner},
        editor    = {Michael Hind and
                     Amer Diwan},
        title     = {Proving Optimizations Correct using
                     Parameterized Program Equivalence},
        booktitle = {Proceedings of the 2009 {ACM} {SIGPLAN} Conference on
                     Programming Language Design and Implementation,
                     {PLDI} 2009,
                     Dublin, Ireland,
                     June 15-21, 2009},
        pages     = {327--337},
        publisher = {{ACM}},
        year      = {2009},
        url       = {https://doi.org/10.1145/1542476.1542513},
        doi       = {10.1145/1542476.1542513},
      }
      

Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Principles of Programming Languages (POPL) 2009
paper   talk   slides   code   project  


      @inproceedings{,
        author    = {Ross Tate and
                     Michael Stepp and
                     Zachary Tatlock and
                     Sorin Lerner},
        editor    = {Zhong Shao and
                     Benjamin C. Pierce},
        title     = {Equality Saturation: A New Approach to Optimization},
        booktitle = {Proceedings of the 36th {ACM} {SIGPLAN-SIGACT} Symposium on
                     Principles of Programming Languages,
                     {POPL} 2009,
                     Savannah, GA, {USA},
                     January 21-23, 2009},
        pages     = {264--276},
        publisher = {{ACM}},
        year      = {2009},
        url       = {https://doi.org/10.1145/1480881.1480915},
        doi       = {10.1145/1480881.1480915},
      }

Deep Typechecking and Refactoring
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2008
paper   slides   poster   project  


      @inproceedings{2008-oopsla-quail-deep-typechecking-and-refactoring,
        author    = {Zachary Tatlock and
                     Chris Tucker and
                     David Shuffelton and
                     Ranjit Jhala and
                     Sorin Lerner},
        editor    = {Gail E. Harris},
        title     = {Deep Typechecking and Refactoring},
        booktitle = {Proceedings of the 23rd Annual {ACM} {SIGPLAN} Conference on
                     Object-Oriented Programming, Systems, Languages, and Applications,
                     {OOPSLA} 2008,
                     Nashville, TN, {USA},
                     October 19-23, 2008},
        pages     = {37--52},
        publisher = {{ACM}},
        year      = {2008},
        url       = {https://doi.org/10.1145/1449764.1449768},
        doi       = {10.1145/1449764.1449768},
      }
      

 

Aggregators