Pavel Panchekha


Share under CC-BY-SA.

Pavel Panchekha

I am an Assistant Professor at the University of Utah.

I study mechanical reasoning and synthesis for domain-specific languages, such as floating-point numerical programs and web page layout code.

Table of Contents


egg: Fast and Extensible Equality Saturation arxiv
POPL'21: Willsey, Nandi, Wang, Flatt, Tatlock, Panchekha
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 doi
PLDI’14: Sampson, Panchekha, Mytkowicz, McKinley, Grossman, & Ceze


Google Faculty Research Award (2020)

Adobe Research Fellowship (2016)

NSF Graduate Research Fellow (2015)

PLDI Distinguished Paper Award (2015)

NSF Graduate Research Fellowship, Honorable Mention (2014)

Wissner-Slivka Endowed Graduate Fellowship (2013)

Achievement Rewards for College Scientists Fellow (2013)


PLDI 2021 PC, Member

ASPLOS 2021 ERC, Member

POPL 2021 AEC, Co-chair

FPTalks 2020, Chair

PLDI 2020 SRC, Member

University of Utah School of Computing, Admissions Committee Member, 2020

PLDI 2020 ERC, Member

University of Utah School of Computing, Diversity Committee Member, 2019

J. Software: Practice and Experience, Reviewer, 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.


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

  • Focus on programming languages, verification, and synthesis
  • Advised by Michael D. Ernst and Zachary Tatlock
  • Ph.D. candidacy in Computer Science (awarded 2017)
  • Master's degree in Computer Science (awarded 2015)
  • Courses: programming languages, sublinear algorithms, data visualization, machine learning, natural language processing, program synthesis

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

  • Mathematics Major (Course 18); 4.7 GPA
  • Advanced CS courses: distributed systems, security, symbolic reasoning, advanced algorithms
  • Advanced mathematics courses: commutative algebra, differential geometry, stochastic processes, computational ring theory