Oded Padon I am a researcher at VMware Research Group. Before that, I was a postdoc in Alex Aiken's group at Stanford University. Before that, I was a PhD student at Tel Aviv University, advised by Mooly Sagiv. My research interests are programming languages, formal methods, logic, and distributed systems. You may be interested in: Ivy a system for verifying safety and liveness of distributed algorithms and distributed system implementations using decidable logics. TASO Tensor Algebra SuperOptimizer that optimizes deep learning computations using automatically generated and verified graph transformations, achieving up to 3x speedup over other frameworks. mypyvy a research platform for verification of infinite-state systems, inspired by Ivy. How far can you EPR? a 30 minute talk summarizing my PhD research given at the virtual ETAPS 2020 Afternoon upon receiving the 2020 ETAPS Doctoral Dissertation Award.

Publications

(dblp) (google scholar)

• Adaptive Restarts for Stochastic Synthesis (pdf)
  Jason R. Koenig, Oded Padon, Alex Aiken. PLDI 2021.
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (pdf) (artifact)
  Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett. TACAS 2021.
• Ivy: A Multi-modal Verification Tool for Distributed Algorithms (tool paper) (pdf) (tool)
  Kenneth L. McMillan, Oded Padon. CAV 2020.
• First-Order Quantified Separators (pdf) (artifact) (source code)
  Jason R. Koenig, Oded Padon, Neil Immerman, Alex Aiken. PLDI 2020.
• SPoC: Search-based Pseudocode to Code (pdf) (web)
  Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, Percy Liang. NeurIPS 2019.
• TASO: Optimizing Deep Learning Computation with Automated Generation of Graph Substitutions (pdf) (tool)
  Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia, Alex Aiken. SOSP 2019.
• Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics (pdf) (extended)
  Idan Berkovits, Marijana Lazic, Giuliano Lossa, Oded Padon, Sharon Shoham. CAV 2019.
• Semantic Program Alignment for Equivalence Checking (pdf) (source code)
  Berkeley Churchill, Oded Padon, Rahul Sharma, Alex Aiken. PLDI 2019.
• Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems (pdf)
  Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham. FMCAD 2018.
• Deductive Verification in Decidable Fragments with Ivy (pdf)
  Kenneth L. McMillan, Oded Padon. SAS 2018.
• Modularity for Decidability of Deductive Verification with Applications to Distributed Systems (pdf) (web)
  Marcelo Taube, Giuliano Losa, Kenneth McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos. PLDI 2018.
• Reducing Liveness to Safety in First-Order Logic (pdf) (source files) (web) (video)
  Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham. POPL 2018.
• Paxos Made EPR: Decidable Reasoning about Distributed Protocols
  Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham. OOPSLA 2017.
  (pdf) (full) (source files) (web) (video)
• RATCOP: Relational Analysis Tool for Concurrent Programs (tool paper) (pdf) (tool)
  Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky. HVC 2017.
• Thread-Local Semantics and its Efficient Sequential Abstractions for Race-Free Programs (pdf)
  Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky. SAS 2017. Radhia Cousot Young Researcher Best Paper Award.
• Bounded Quantifier Instantiation for Checking Inductive Invariants
  Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham. TACAS 2017.
  (pdf) (extended) (source files)
• Conjunctive Abstract Interpretation using Paramodulation (pdf) (tool)
  Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv. VMCAI 2017.
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors (pdf)
  Asya Frumkin, Yotam M. Y. Feldman, Ondřej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham. VMCAI 2017.
• Ivy: Safety Verification by Interactive Generalization (pdf) (tool) (artifact) (video)
  Oded Padon, Kenneth McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham. PLDI 2016.
• Decidability of Inferring Inductive Invariants (pdf) (video)
  Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv. POPL 2016.
• Decentralizing SDN Policies (pdf)
  Oded Padon, Neil Immerman, Ori Lahav, Aleksandr Karbyshev, Mooly Sagiv, Sharon Shoham. POPL 2015.

PhD Thesis

Deductive Verification of Distributed Protocols in First-Order Logic (pdf)
School of Computer Science, Tel Aviv University, Israel. Submitted: 2018; Approved: 2019.

Recipient of the 2020 ETAPS Doctoral Dissertation Award.

During my PhD I was honored to be awarded a 2017 Google PhD Fellowship in programming languages.

Teaching

Tel Aviv University

• Workshop in Verifying Distributed Algorithms (Spring 2017-2018)
• Advanced Topics in Programming Languages (Fall 2017-2018)
• Concepts in Programming Languages
  • Spring 2017-2018
  • Winter 2016-2017
  • Spring 2015-2016
  • Spring 2014-2015
• Programming in Python for Engineers (Fall 2015-2016)
• Automatic Software Verification (Spring 2014-2015)