ztatlock@cs.washington.edu
https://ztatlock.net
I am a Professor in the Allen School at the University of Washington. I work with students in the UW PLSE group on formal methods, compilers, equality saturation, numerics, and fabrication, with an emphasis on making difficult software easier to build and reason about. My work combines formal semantics and verification with practical systems, tools, and measurements.
Current scale: 8 current students and postdocs; 12 graduated PhD students; 69 indexed publications; 1,600+ UW students taught over 28 course offerings.
University of Washington, Seattle, WA
Paul G. Allen School of Computer Science & Engineering
Professor, Autumn 2024 – Present
Associate Professor, Autumn 2019 – Autumn 2024
Assistant Professor, Autumn 2014 – Autumn 2019
Acting Assistant Professor, Autumn 2013 – Autumn 2014
Amazon Web Services, Seattle, WA
Automated Reasoning Group
Amazon Scholar, Autumn 2021 – Spring 2025
OctoML, Seattle, WA
Compiler Design and Implementation Group
Advisor, Autumn 2019 – Spring 2021
Microsoft Research India, Bengaluru, India
Systems Research Group
Graduate Research Intern, Summer 2010
University of California, San Diego, CA
PhD, Computer Science & Engineering, Autumn 2014
Thesis: Reducing the Costs of Proof Assistant Based Formal Verification
Advisor: Sorin Lerner
Purdue University, West Lafayette, IN
BS, Computer Science (Honors), Spring 2007
BS, Mathematics, Spring 2007
Advisor: Suresh Jagannathan
Target-Aware Implementation of Real Expressions
Brett Saiki, Jackson Brough, Jonas Regehr, Jesús Ponce, Varun Pradeep, Aditya Akhileshwaran, Zachary Tatlock, Pavel Panchekha
Architectural Support for Programming Languages and Operating Systems 2025
Computational Illusion Knitting
Amy Zhu, Yuxuan Mei, Benjamin Jones, Zachary Tatlock, Adriana Schulz
ACM Transactions on Graphics 2024
Magic Markup: Maintaining Document-External Markup with an LLM
Edward Misback, Zachary Tatlock, Steven L. Tanimoto
<Programming> 2024
FPGA Technology Mapping Using Sketch-Guided Program Synthesis
Gus Henry Smith, Benjamin Kushigian, Vishal Canumalla, Andrew Cheung, Steven Lyubomirsky, Sorawee Porncharoenwase, René Just, Gilbert Louis Bernstein, Zachary Tatlock
Architectural Support for Programming Languages and Operating Systems 2024
Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface
Bo-Yuan Huang, Steven Lyubomirsky, Yi Li, Mike He, Gus Henry Smith, Thierry Tambe, Akash Gaonkar, Vishal Canumalla, Andrew Cheung, Gu-Yeon Wei, Aarti Gupta, Zachary Tatlock, Sharad Malik
ACM Transactions on Design Automation of Electronic Systems 2024
Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting
Edward Misback, Caleb C. Chan, Brett Saiki, Eunice Jun, Zachary Tatlock, Pavel Panchekha
ACM Symposium on User Interface Software and Technology 2023
Equality Saturation Theory Exploration à la Carte
Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi
Object-Oriented Programming, Systems, Languages & Applications 2023
Better Together: Unifying Datalog and Equality Saturation
Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey
Programming Language Design and Implementation 2023
babble: Learning Better Abstractions with E-Graphs and Anti-Unification
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova
Principles of Programming Languages 2023
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha
Formal Methods in Computer-Aided Design 2022
Verified Compilation and Optimization of Floating-Point Programs in CakeML
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony Fox
European Conference on Object-Oriented Programming 2022
Co-Optimization of Design and Fabrication Plans for Carpentry
Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz
ACM Transactions on Graphics 2022
Relational e-matching
Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock
Principles of Programming Languages 2022
Rewrite Rule Inference Using Equality Saturation
Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock
Object-Oriented Programming, Systems, Languages & Applications 2021
★ Distinguished Paper
A Roadmap Towards Parallel Printing for Desktop 3D Printers
Molly Aubrey Carton, Chandrakana Nandi, Adam Anderson, Haisen Zhao, Eva Darulova, Dan Grossman, Jeffrey I. Lipton, Adriana Schulz, Zachary Tatlock
Solid Freeform Fabrication Symposium 2021
Pure Tensor Program Rewriting via Access Patterns
Gus Henry Smith, Andrew Liu, Steven Lyubomirsky, Scott Davidson, Joseph McMahan, Michael Taylor, Luis Ceze, Zachary Tatlock
Symposium on Machine Programming 2021
Combining Precision Tuning and Rewriting
Brett Saiki, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock
IEEE International Symposium on Computer Arithmetic 2021
Dynamic Tensor Rematerialization
Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock
International Conference on Learning Representations 2021
★ Spotlight Paper
Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference
Haichen Shen, Jared Roesch, Zhi Chen, Wei Chen, Yong Wu, Mu Li, Vin Sharma, Zachary Tatlock, Yida Wang
Conference on Machine Learning and Systems 2021
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha
Principles of Programming Languages 2021
★ Distinguished Paper
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 2020
Carpentry Compiler
Chenming Wu, Haisen Zhao, Chandrakana Nandi, Jeffrey I. Lipton, Zachary Tatlock, Adriana Schulz
SIGGRAPH Asia, ACM Transactions on Graphics 2019
Modular Verification of Web Page Layout
Pavel Panchekha, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Object-Oriented Programming, Systems, Languages & Applications 2019
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 2019
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
Computer-Aided Verification 2019
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 2019
Sinking Point: Dynamic Precision Tracking for Floating-point
Bill Zorn, Dan Grossman, Zachary Tatlock
Conference for Next Generation Arithmetic 2019
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 2018
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock
Formal Methods 2018
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 2018
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 2018
Finding Root Causes of Floating Point Error
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
Programming Language Design and Implementation 2018
Verifying that Web Pages have Accessible Layout
Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Programming Language Design and Implementation 2018
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman
Certified Programs and Proofs 2018
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, Zachary Tatlock
Principles of Programming Languages 2018
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 2017
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 2017
Programming Language Abstractions for Modularly Verified Distributed Systems
James R. Wilcox, Ilya Sergey, Zachary Tatlock
Summit oN Advances in Programming Languages 2017
Programming Language Tools and Techniques for 3D Printing
Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock
Summit oN Advances in Programming Languages 2017
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 2016
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 2016
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 2016
Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman
Programming Language Design and Implementation 2016
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 2016
Automatically Improving Accuracy for Floating Point Expressions
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock
Programming Language Design and Implementation 2015
★ Distinguished Paper
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 2015
RoboFlow: A Flow-based Visual Programming Language for Mobile Manipulation Tasks
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
International Conference on Robotics and Automation 2015
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 2015
Visual Robot Programming for Generalizable Mobile Manipulation Tasks
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
Human Robot Interaction 2015
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
Operating Systems Design and Implementation 2014
Automating Formal Proofs for Reactive Systems
Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation 2014
SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks
Dongseok Jang, Zachary Tatlock, Sorin Lerner
Network and Distributed System Security 2014
Establishing Browser Security Guarantees through Formal Shim Verification
Dongseok Jang, Zachary Tatlock, Sorin Lerner
USENIX Security Symposium 2012
Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Logical Methods in Computer Science 2011
Bringing Extensibility to Verified Compilers
Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation 2010
Proving Optimizations Correct using Parameterized Program Equivalence
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation 2009
Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Principles of Programming Languages 2009
Deep Typechecking and Refactoring
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
Object-Oriented Programming, Systems, Languages & Applications 2008
Exploring Self-Embedded Knitting Programs with Twine
Amy Zhu, Adriana Schulz, Zachary Tatlock
ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design 2023
Generate Compilers from Hardware Models!
Gus Henry Smith, Ben Kushigian, Vishal Canumalla, Andrew Cheung, René Just, Zachary Tatlock
Workshop on Programming Languages and Computer Architecture 2023
Guarding Numerics Amidst Rising Heterogeneity
Ganesh Gopalakrishnan, Ignacio Laguna, Ang Li, Pavel Panchekha, Cindy Rubio-González, Zachary Tatlock
Software Correctness for HPC Applications 2021
From DSLs to Accelerator-Rich Platform Implementations: Addressing the Mapping Gap
Bo-Yuan Huang, Steven Lyubomirsky, Thierry Tambe, Yi Li, Mike He, Gus Henry Smith, Gu-Yeon Wei, Aarti Gupta, Sharad Malik, Zachary Tatlock
Workshop on Languages, Tools, and Techniques for Accelerator Design 2021
Towards Numerical Assistants
Pavel Panchekha, Zachary Tatlock
Numerical Software Verification 2020
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 2020
Toward Multi-Precision, Multi-Format Numerics
David Thien, Bill Zorn, Pavel Panchekha, Zachary Tatlock
Software Correctness for HPC Applications 2019
Theia: Automatically Generating Correct Program State Visualizations
Josh Pollock, Jared Roesch, Doug Woos, Zachary Tatlock
ACM SIGPLAN International Symposium on SPLASH-E 2019
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 2017
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 2016
Peek: A Formally Verified Peephole Optimization Framework for x86
Eric Mullen, Zachary Tatlock, Dan Grossman
Workshop on Coq for Programming Languages 2015
Chapter 8: Parameterized Program Equivalence Checking
High-Level Verification: Methods and Tools for Verification of System-Level Designs
Sudipta Kundu, Sorin Lerner, and Rajesh K. Gupta; Springer 2011
UW CSE 507: Computer-Aided Reasoning for Software
Graduate course introducing automated reasoning techniques for the design, analysis, and construction of software
UW CSE 505: Concepts of Programming Languages
Graduate course using proof assistants to explore transition systems, inductive invariants, type systems, Hoare logic, metatheory
UW CSE 341: Programming Languages
Undergraduate course exploring informal operational semantics, functional programming vs. OOP, static vs. dynamic typing
UW CSE 331: Software Design and Implementation
Undergraduate course exploring specification, invariants, testing, debugging, modular design
Special Topics Graduate Courses
★ I was honored to be nominated for the UW Distinguished Teaching Award in 2015.
DeepSpec Summer School 2018
Verifying Distributed Systems Implementations in Coq
Marktoberdorf Summer School 2024
Analysis and Optimizations with Equality Saturation
UCSD CSE 231: Advanced Compiler Design
Graduate course exploring program analyses and compiler optimizations
UCSD CSE 130: Programming Languages
Undergraduate course exploring functional programming, static vs. dynamic typing, and logic programming
Purdue CS 180: Introduction to Java Programming
Undergraduate course introducing students to Java programming: variables, conditionals, loops, recursion, testing, modular design, and basic systems programming
Distinguished Paper Award for “Rewrite Rule Inference Using Equality Saturation”
ACM SIGPLAN Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2021
Spotlight Paper Award for “Dynamic Tensor Rematerialization”
International Conference on Learning Representations (ICLR) 2021
Distinguished Paper Award for “egg: Fast and Extensible Equality Saturation”
ACM SIGPLAN Principles of Programming Languages (POPL) 2021
Faculty Appreciation for Career Education & Training (FACET) Award
University of Washington, 2020
NSF CAREER Award: Verifying Distributed System Implementations
National Science Foundation, 2017
Distinguished Paper Award for “Automatically Improving Accuracy for Floating Point Expressions”
ACM SIGPLAN Programming Language Design and Implementation (PLDI) 2015
Distinguished Teaching Award Nomination
University of Washington, 2015
Everything is a compiler, try Equality Saturation!
Brown University, PL and Graphics groups, February 2026
When You’ve Got EqSat, Everything Is a Compiler
Cornell University, November 2024
Analysis and Optimizations with Equality Saturation
Marktoberdorf Summer School, August 2024
Relational Equality Saturation in egg
Synopsys Inc., Fall 2023
Relational Equality Saturation in egg
Adobe Inc., Fall 2023
Relational Equality Saturation in egg
University of Illinois at Urbana-Champaign, Compilers Seminar, May 2023
The egg Equality Saturation Toolkit
UC San Diego, Databases Seminar, March 2023
The egg Equality Saturation Toolkit
ETH Workshop on Dependable and Secure Software Systems, October 2022
Programming Languages for the Next Manufacturing Revolution
Department of Energy, July 2022
Towards Optimizing Multi-precision, Multi-format Numerical Codes
Intel ARITH, October 2020
Synthesizing Backward through the Geometry Pipeline
University of Wisconsin, PL Seminar, August 2020
Towards Numerical Assistants
Numerical Software Verification @ CAV, July 2020
Synthesis of Floating Point Programs and Beyond
Synthetic Minds, September 2019
TVM Relay: A Functional IR for Analysis and Optimization
TVM Conference, May 2019
Verifying Implementations of Distributed Systems
Galois Inc., September 2018
Formally Verifying Implementations of Distributed Systems
Princeton University, DeepSpec Summer School, July 2018
Formally Verifying Implementations of Distributed Systems
Oxford University, Coq Workshop at FLOC, July 2018
Navigating Your Career Path
Programming Languages Mentoring Workshop (PLMW), June 2018
Automatically Improving the Accuracy of Floating Point Expressions
Max Planck Institute (MPI-SWS Saarbrüken), August 2017
The FPBench Suite and Specification
Dagstuhl on Analysis and Synthesis of Floating-point Programs, August 2017
Verifying Control Plane Policies in BGP
Mathematical Foundations of Programming Semantics (MFPS), June 2017
Automated Formal Verification for Border Gateway Protocol Configurations
Purdue University, April 2017
Automatically Improving the Accuracy of Floating Point Expressions
University of Utah, February 2017
Dijkstra and De Millo: Challenges in Applying and Teaching Verification
Microsoft Research Faculty Summit, July 2016
Verifying Safety Cases for Radiotherapy Control
Verified Software: Theories, Tools, and Experiments (VSTTE), June 2016
ICFP 2026, Program Committee
ARITH 2023, Program Committee
ASPLOS 2023, External Review Committee
NSF 2023, Grant Review Panel
PLDI 2023, Program Committee
ARITH 2022, Program Committee
ASPLOS 2021, Program Committee
PLDI 2021, Program Committee
ASPLOS 2020, Program Committee
OOPSLA 2020, External Review Committee
PLDI 2020, External Program Committee
SCF 2020, External Reviewer
CPP 2019, Program Committee
ICFP 2019, External Review Committee
PLDI 2019, Program Committee
ITP 2018, Program Committee
POPL 2018, Program Committee
TOPLAS 2018, Referee
ASPLOS 2017, External Reviewer
Onward! 2017, Program Committee
POPL 2017, External Reviewer
ASPLOS 2016, External Review Committee
CPP 2016, Program Committee
PLDI 2016, Program Committee
PLDI Artifact Evaluation Committee 2016, Co-Chair
POPL 2016, External Review Committee
CoqPL 2015, Program Committee
POPL 2015, External Review Committee
OOPSLA 2014, External Review Committee
PLDI 2014, External Review Committee
CC 2009, External Reviewer
PACMPL Advisory Board Member, 2026 - 2029
PLDI Steering Committee, 2026 - 2029
EGRAPHS Community Advisory Board, 2022 - Present
ISCSA Tutorial: Generalizing the ISA to the ILA 2022, Co-Organizer
PLDI Tutorial: Build Your Optimizer with egg 2022, Co-Organizer
SRC JUMP: Applications Driving Architectures (ADA) Student Hackathon Organizer, 2019 - 2020
University of Washington Verification in Practice (ViP) 2019, Co-Organizer
PLDI Programming Languages Mentoring Workshop (PLMW) 2018, Panelist
POPL Programming Languages Mentoring Workshop (PLMW) 2018, Panelist
SPLASH Doctoral Symposium 2017, Program Committee
UW NSF STARS 2017, Mentor
POPL Student Research Competition (SRC) 2016, Organizer
PLDI Student Research Competition (SRC) 2015, Committee
SPLASH Programming Languages Mentoring Workshop (PLMW) 2015, Co-Chair
SPLASH Inspirations 2014, Co-Organizer and Speaker
UW CSE Faculty Graduate Admissions Co-chair, 2025 - 2027
UW CSE Faculty Recruiting Co-chair, 2022 - 2024
UW CSE Distinguished Lecture and Colloquia Organizer, 2018 - 2021
UW CSE Undergraduate Admissions Committee, 2020 - 2021
UW CSE Diversity Committee, 2019 - 2020
UW CSE Grad Culture Chair, 2013 - 2019
UW CSE Graduate Admissions Committee, 2018 - 2019
UW CSE BSMS Admissions Committee, 2016 - 2018
UW CSE Undergraduate Admissions Committee, 2017 - 2018
UW CSE Visit Days Organizing Committee, 2015 - 2016
UCSD GradCom Student Representative, 2009 - 2011
I have also helped write, produce, and direct UW’s annual faculty skit since 2015 with Hank Levy and Adriana Schulz.
ComPort: Rigorous Testing Methods to Safeguard Software Porting
Co-PI; DOE; $405,000; 2021 – 2024
V-SPELLS: POLYMORPH: Promotion to Optimal Languages Yielding Modular Operator-driven Replacements and Programmatic Hooks
Co-PI; DARPA; $746,365; 2021 – 2024
FMitF: Retargetable, Verifiable, Optimizable Computer-Aided Manufacturing
Co-PI; NSF CCF-2017927; $749,913; 2020 – 2023
RTML: Automatic Synthesis of HW/SW Systems for General Neural-Networks
Co-PI; DARPA; $2,803,490; 2019 – 2022
Knit Pattern Understanding for Garment Modeling, Modification, and Fabrication
Co-PI; NSF CHS-1907337; $500,000; 2019 – 2021
FMitF: Formal Verification of Accessibility
Co-PI; NSF CCF-1836813; $738,125; 2019 – 2022
Programming Languages Foundations for 3D Printing
PI; NSF SHF-1813166; $500,000; 2018 – 2021
Applications Driving Architectures (ADA) SRC JUMP Center
Co-PI; Joint SRC & DARPA; $580,000; 2018 – 2022
CAREER: Verifying Distributed Systems Implementations
PI; NSF CCF-1749570; $550,000; 2018 – 2023
BRASS: A Picture is Worth a Billion Bits: Adaptive Visualization of Big Data
Co-PI; DARPA; $7,500,000; 2015 – 2019