Pavel Panchekha

Target-Aware Implementation of Real Expressions
ASPLOS'25: Saiki, Brough, Regehr, Ponce, Pradeep, Akhileshwaran, Tatlock, Panchekha

Implementation and Synthesis of Math Library Functions
POPL'24: Briggs, Lad, Panchekha doi arxiv talk
Distinguished Paper

Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting
UIST'23: Misback, Chan, Saiki, Jun, Tatlock, Panchekha doi arxiv

Making Interval Arithmetic Robust to Overflow
ARITH'23: Flatt, Panchekha conf arxiv

Optimal Heap Limits for Reducing Browser Memory Use
OOPSLA'22: Kirisame, Shenoy, Panchekha doi arxiv

Small Proofs from Congruence Closure
FMCAD'22: Flatt, Coward, Willsey, Tatlock, Panchekha doi arxiv

Choosing Mathematical Function Implementations for Speed and Accuracy
PLDI'22: Briggs, Panchekha doi

Combining Precision Tuning and Rewriting
ARITH'21: Saiki, Flatt, Panchekha, Tatlock doi

egg: Fast and Extensible Equality Saturation
POPL'21: Willsey, Nandi, Wang, Flatt, Tatlock, Panchekha doi
Distinguished Paper

Scalable yet Rigorous Floating-Point Error Analysis
SC'20: Das, Briggs, Gopalakrishnan, Krishnamoorthy, Panchekha doi
Best Student Paper

Modular Verification of Web Page Layout
OOPSLA’19: Panchekha, Ernst, Tatlock, & Kamil doi

Functional Programming for Compiling and Decompiling Computer-Aided Design
ICFP’18: Nandi, Wilcox, Panchekha, Blau, Grossman, & Tatlock doi

Verifying that Web Pages have Accessible Layout
PLDI’18: Panchekha, Geller, Ernst, Tatlock, & Kamil doi

Finding Root Causes of Floating Point Error
PLDI’18: Sanchez-Stern, Panchekha, Lerner, & Tatlock doi

Automated Reasoning for Web Page Layout
OOPSLA’16: Panchekha, & Torlak doi

Automatically Improving Accuracy for Floating Point Expressions
PLDI’15: Panchekha, Sanchez-Stern, Wilcox, & Tatlock doi
Distinguished Paper

Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
PLDI’15: Wilcox, Woos, Panchekha, Tatlock, Wang, Ernst, & Anderson doi

Expressing and Verifying Probabilistic Assertions
PLDI’14: Sampson, Panchekha, Mytkowicz, McKinley, Grossman, & Ceze doi

CS 3550, Web Software Development I (Fall 2023, Fall 2024)

CS 4560, Web Browser Internals (Fall 2019, Fall 2021, Spring 2024)

CS 4470, Compilers (Spring 2021, Spring 2023)

CS 2100, Discrete Structures (Spring 2022)

CS 6110, Software Verification (Spring 2020)

Chair: POPL 2022 AEC, FPTalks 2021, POPL 2021 AEC, FPTalks 2020

Panel: NSF 2024

PC: POPL 2025, ARITH 2024, OOPSLA 2024, ARITH 2023, POPL 2022, PLDI 2021

ERC/Special: ASPLOS 2025, PLDI 2024, ASPLOS 2021, PLDI 2020

Other: Correctness 2024, SDD 2023, PLDI 2021 SRC, PLDI 2016 AEC

Internal: Undergrad Research (2023–), GradSAC 2020–, Website 2020–2023, Diversity 2019–2022, Admissions 2020

Dean's teaching recognition (2021)

V8 Research Grant (2021)

Google Faculty Research Award (2020)

Adobe Research Fellowship (2016)

NSF Graduate Research Fellowship (2015)

NSF Graduate Research Fellowship, Honorable Mention (2014)

Wissner-Slivka Endowed Graduate Fellowship (2013)

Achievement Rewards for College Scientists (2013)

Assistant Professor in CS at the University of Utah (2019–)

Ph.D. in CS at the University of Washington (2013–2019)

• Advised by Michael D. Ernst and Zachary Tatlock
• Ph.D. candidacy in Computer Science (awarded 2017)
• Master's degree in Computer Science (awarded 2015)

B.S. in Mathematics at the Massachusetts Institute of Technology (2010–2013)

Incremental Bidirectional Typing via Order Maintenance
WITS'25: Porter, Kirisame, Mulcahy, Panchekha, Omar

Synthesizing Mathematical Identities with E-graphs
EGRAPHS'22: Briggs, Panchekha doi

Correctness-preserving Compression of Datasets and Neural Network Models
Correctness'20: Joseph, Chalapathi, Bhaskara, Gopalakrishnan, Panchekha, Zhang doi

Towards Multi-Precision, Multi-Format Numerics
Correctness’19: Thien, Zorn, Panchekha, & Tatlock doi

Combining Tools for Optimization and Analysis of Floating-Point Computations
FM’18 short: Becker, Panchekha, Darulova, & Tatlock doi

Generating Interactive Web Pages from Storyboards
FSE’16 doctoral symposium: Panchekha doi

Toward a Standard Benchmark Format and Suite for Floating-Point Analysis
NSV’16: Damouche, Martel, Panchekha, Qiu, Sanchez-Stern, & Tatlock doi

Blame Trees
WADS’13: Demaine, Panchekha, Wilson, & Yang doi

Distributed Shared State with History Maintenance
MIT technical report 2013, Panchekha & Brodsky doi

Virtual Machines for Graphics Code
Apr 2023, invited talk, Adobe Research

FPBench: Standards, benchmarks, and tools for the floating point community
Nov 2021, keynote, Intel ARITH 2021

Towards Numerical Assistants
July 2020, keynote, NSV 2020

FPCore: Standard Format for FP Analysis Tools
November 2019, tutorial, Supercomputing 2019

Verifying Web Pages
October 2019, seminar, MIT
October 2019, seminar, Harvard
October 2019, invited talk, University of Massachusetts (Amherst)
September 2019, research forum, Utah
September 2019, invited talk, State of the Art in Program Synthesis
August 2019, colloquium, Utah
July 2019, invited talk, MSR
March 2019, invited talk, Purdue
February 2019, invited talk, University of Utah
September 2018, invited talk, RacketCon
September 2018, seminar, UW
May 2018, invited talk, PNW PLSE

Numerical Tools for Non-expert Users
January 2018, invited talk, MSR Redmond.
August 2017, Dagstuhl.
August 2017, invited talk, MPI-SWS Saarbrücken.

Automatically Improving Accuracy for Floating Point Expressions
April 2016, invited talk, Google.
March 2016, seminar, MIT.
January 2016, invited talk, MathWorks.
October 2015, seminar, UW CSE Affiliates Day.
October 2015, seminar, University of Washington.
January 2015, invited talk, Reservior Labs.
March 2014, invited talk, Dropbox.

Next-generation Eventual Consistency
January 2015, invited talk, Facebook.

Adobe (2016): automatic reasoning framework for web page layout

Dropbox (2013): model checking for synchronization algorithms

MIT CSAIL (2011–2012): novel eventually-consistent shared state algorithm.

MIT Mathematics (2012): parallelized elliptic curve point-counting computation.

Dropbox (2011): wrote distributed profiler for server farms.

Fairleigh Dickinson University (2009–2010): autonomous jeep control