Pavel Panchekha


Share under CC-BY-SA.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

Pavel Panchekha

I am a Ph.D. Candidate at the University of Washington, graduating in 2019.

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

Table of Contents


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 System
PLDI’15: Wilcox, Woos, Panchekha, Tatlock, Wang, Ernst, & Anderson doi

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


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)


Ph.D. Candidate 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


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.

Minor Papers

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


Verifying Web Pages
September 2018, invited talk, RacketCon
September 2018, CSE Symposium, UW
May 2018, 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, invited talk, MIT.
January 2016, invited talk, MathWorks.
October 2015, invited talk, UW CSE Affiliates Day.
October 2015, Numerical Analysis Research Club at the University of Washington.
January 2015, invited talk, Reservior Labs.
March 2014, invited talk, Dropbox.

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