|
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)- 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.