Oded Padon
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
28
Venues
9
Active years
2015–2026
Best venue rank
A*
Where they publish
Papers
28 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | Lagrangian-Based Duality for Quantified SMT Algorithms. | Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham |
| 2026 | TACAS | Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings. | Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham |
| 2025 | OSDI | Mirage: A Multi-Level Superoptimizer for Tensor Programs. | Mengdi Wu, Xinhao Cheng, Shengyu Liu, Chunan Shi, Jianan Ji, Man Kit Ao, Praveen Velliengiri, Xupeng Miao, Oded Padon, Zhihao Jia |
| 2024 | CAV | Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. | Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham |
| 2024 | CAV | mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic. | James R. Wilcox, Yotam M. Y. Feldman, Oded Padon, Sharon Shoham |
| 2024 | OSDI | Anvil: Verifying Liveness of Cluster Management Controllers. | Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, Tianyin Xu |
| 2024 | SOSP | Verus: A Practical Foundation for Systems Verification. | Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, Bryan Parno |
| 2022 | FMCAD | Verification of Distributed Protocols: Decidable Modeling and Invariant Inference. | Oded Padon |
| 2022 | PLDI | Quartz: superoptimization of Quantum circuits. | Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia |
| 2022 | TACAS | Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. | Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken |
| 2021 | PLDI | Adaptive restarts for stochastic synthesis. | Jason R. Koenig, Oded Padon, Alex Aiken |
| 2021 | TACAS | Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. | Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett |
| 2020 | CAV | Ivy: A Multi-modal Verification Tool for Distributed Algorithms. | Kenneth L. McMillan, Oded Padon |
| 2020 | PLDI | First-order quantified separators. | Jason R. Koenig, Oded Padon, Neil Immerman, Alex Aiken |
| 2019 | CAV | Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. | Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham |
| 2019 | PLDI | Semantic program alignment for equivalence checking. | Berkeley R. Churchill, Oded Padon, Rahul Sharma, Alex Aiken |
| 2019 | SOSP | TASO: optimizing deep learning computation with automatic generation of graph substitutions. | Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia, Alex Aiken |
| 2018 | FMCAD | Deductive Verification of Distributed Protocols in First-Order Logic. | Oded Padon |
| 2018 | FMCAD | Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. | Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham |
| 2018 | PLDI | Modularity for decidability of deductive verification with applications to distributed systems. | Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos |
| 2018 | SAS | Deductive Verification in Decidable Fragments with Ivy. | Kenneth L. McMillan, Oded Padon |
| 2017 | SAS | Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. | Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky |
| 2017 | TACAS | Bounded Quantifier Instantiation for Checking Inductive Invariants. | Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham |
| 2017 | VMCAI | Property Directed Reachability for Proving Absence of Concurrent Modification Errors. | Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhotk, Oded Padon, Mooly Sagiv, Sharon Shoham |
| 2017 | VMCAI | Conjunctive Abstract Interpretation Using Paramodulation. | Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv |
| 2016 | PLDI | Ivy: safety verification by interactive generalization. | Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham |
| 2016 | POPL | Decidability of inferring inductive invariants. | Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv |
| 2015 | POPL | Decentralizing SDN Policies. | Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham |