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.

Publications

(dblp) (google scholar)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification (pdf) (extended) (artifact)
Neta Elad, Oded Padon, Sharon Shoham. POPL 2024.
Leaf: Modularity for Temporary Sharing in Separation Logic (pdf) (extended) (artifact)
Travis Hance, Jon Howell, Oded Padon, Bryan Parno. OOPSLA 2023.
Quartz: Superoptimization of Quantum Circuits (pdf) (extended) (artifact) (tool)
Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia. PLDI 2022.
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion (pdf) (artifact)
Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken. TACAS 2022.
Induction Duality: Primal-Dual Search for Invariants (pdf) (artifact)
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken. POPL 2022.
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 (conference pdf) (journal pdf)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham. FMCAD 2018, FMSD 2021.
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