Pavel Panchekha


Share under CC-BY-SA.

Pavel Panchekha

I study mechanical reasoning and synthesis for domain-specific languages, such as floating-point numerical programs and web page layout code, as an Assistant Professor at the University of Utah.

Table of Contents


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

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

Appointments and Education

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)


Google Faculty Research Award (2020)

Adobe Research Fellowship (2016)

NSF Graduate Research Fellowship (2015)

PLDI Distinguished Paper Award (2015)

NSF Graduate Research Fellowship, Honorable Mention (2014)

Wissner-Slivka Endowed Graduate Fellowship (2013)

Achievement Rewards for College Scientists (2013)


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

PC: POPL 2022, PLDI 2021

ERC: ASPLOS 2021, PLDI 2020

Other: PLDI 2021 SRC, PLDI 2016 AEC

Committees: Diversity 2020, Admissions 2020, Diversity 2019

Other Papers

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

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

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


Towards Numerical Assistants
July 2020, keynote, NSV 2020

Welcome, and an Introduction to FPBench
June 2020, invited talk, FPTalks 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 in Cambridge, MA (2016)

  • Extended automatic reasoning framework for web page layout.
  • Added support for positioning, JavaScript, selectors.
  • Applied synthesis to product needs.

Dropbox in San Francisco, CA (2011, 2013)

  • Verified synchronization algorithms & found numerous critical bugs.
  • Wrote distributed profiler for server farms.
  • Designed type system for database schemas.

MIT CSAIL in Cambridge, MA (2012)

  • Worked on eventually-consistent distributed systems.
  • Discovered novel eventually-consistent shared state algorithm.
  • Developed tracing-based debugging tools.

MIT Mathematics in Cambridge, MA (2012)

  • Parallelized elliptic curve point-counting computation.
  • Scale near-linearly to multiple cores (100× speed-up).
  • Developed contribution to Sage mathematics project.

Fairleigh Dickinson University in Hackensack, NJ (2009–2010)

  • Worked on control software for autonomous jeep
  • Taught jeep to drive across unmapped terrain.
  • Built basic artificial intelligence infrastructure for path-finding.