Oded Padon I am 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 verification, logic, and distributed systems. I am honored to be awarded a 2017 Google PhD Fellowship in programming languages.

Publications

• Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems (pdf)
  Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelsk, 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.

Teaching

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