Oded Padon

62 papers A* 13B 7Journal 29Unranked 12
YearRankTypeTitle / Venue / Authors
2026 — conf
On the Power of Temporal Prophecy.
On the Pursuit of Insight and Elegance
Jochen Hoenicke, Oded Padon, Sharon Shoham
2026 — conf
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings.
TACAS (2)
Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham
2026 J jnl
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings.
CoRR
Raz Lotan, Neta Elad, Oded Padon, Sharon Shoham
2025 J jnl
A Primal-Dual Perspective on Program Verification Algorithms (Extended Version).
CoRR
Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham
2025 J jnl
A Primal-Dual Perspective on Program Verification Algorithms.
Proc. ACM Program. Lang.
Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham
2025 A* conf
Mirage: A Multi-Level Superoptimizer for Tensor Programs.
OSDI
Mengdi Wu, Xinhao Cheng, Shengyu Liu, Chunan Shi, Jianan Ji, Man Kit Ao, Praveen Velliengiri, Xupeng Miao, Oded Padon, Zhihao Jia
2024 J jnl
A Multi-Level Superoptimizer for Tensor Programs.
CoRR
Mengdi Wu, Xinhao Cheng, Oded Padon, Zhihao Jia
2024 J jnl
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification.
Proc. ACM Program. Lang.
Neta Elad, Oded Padon, Sharon Shoham
2024 A* conf
Anvil: Verifying Liveness of Cluster Management Controllers.
OSDI
Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, Tianyin Xu
2024 — conf
Clover: Closed-Loop Verifiable Code Generation.
SAIV
Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett
2024 — conf
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas.
CAV (2)
Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
2024 J jnl
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas.
CoRR
Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
2024 J jnl
Quarl: A Learning-Based Quantum Circuit Optimizer.
Proc. ACM Program. Lang.
Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon, Zhihao Jia
2024 A* conf
Verus: A Practical Foundation for Systems Verification.
SOSP
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
2024 — conf
mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic.
CAV (2)
James R. Wilcox, Yotam M. Y. Feldman, Oded Padon, Sharon Shoham
2023 J jnl
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification.
CoRR
Neta Elad, Oded Padon, Sharon Shoham
2023 J jnl
Clover: Closed-Loop Verifiable Code Generation.
CoRR
Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett
2023 — conf
Invited Talk: Deductive Verification of Distributed Protocols in Decidable Logics.
SMT
Oded Padon
2023 J jnl
Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version).
CoRR
Travis Hance, Jon Howell, Oded Padon, Bryan Parno
2023 J jnl
Leaf: Modularity for Temporary Sharing in Separation Logic.
Proc. ACM Program. Lang.
Travis Hance, Jon Howell, Oded Padon, Bryan Parno
2023 J jnl
Quarl: A Learning-Based Quantum Circuit Optimizer.
CoRR
Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon, Zhihao Jia
2022 J jnl
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays.
Log. Methods Comput. Sci.
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
2022 J jnl
Induction duality: primal-dual search for invariants.
Proc. ACM Program. Lang.
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken
2022 — conf
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion.
TACAS (1)
Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken
2022 J jnl
Quartz: Superoptimization of Quantum Circuits (Extended Version).
CoRR
Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia
2022 A* conf
Quartz: superoptimization of Quantum circuits.
PLDI
Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia
2022 B conf
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference.
FMCAD
Oded Padon
2021 A* conf
Adaptive restarts for stochastic synthesis.
PLDI
Jason R. Koenig, Oded Padon, Alex Aiken
2021 — conf
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays.
TACAS (1)
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
2021 J jnl
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays.
CoRR
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett
2021 J jnl
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion.
CoRR
Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken
2021 J jnl
Quanto: Optimizing Quantum Circuits with Automatic Generation of Circuit Identities.
CoRR
Jessica Pointing, Oded Padon, Zhihao Jia, Henry Ma, Auguste Hirth, Jens Palsberg, Alex Aiken
2021 J jnl
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems.
CoRR
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2021 J jnl
Temporal prophecy for proving temporal properties of infinite-state systems.
Formal Methods Syst. Des.
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2020 J jnl
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs.
CoRR
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
2020 A* conf
First-order quantified separators.
PLDI
Jason R. Koenig, Oded Padon, Neil Immerman, Alex Aiken
2020 — conf
Ivy: A Multi-modal Verification Tool for Distributed Algorithms.
CAV (2)
Kenneth L. McMillan, Oded Padon
2020 J jnl
Resources: A Safe Language Abstraction for Money.
CoRR
Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar
2019 J jnl
Bounded Quantifier Instantiation for Checking Inductive Invariants.
Log. Methods Comput. Sci.
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2019 A* conf
SPoC: Search-based Pseudocode to Code.
NeurIPS
Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, Percy Liang
2019 J jnl
SPoC: Search-based Pseudocode to Code.
CoRR
Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, Percy Liang
2019 A* conf
Semantic program alignment for equivalence checking.
PLDI
Berkeley R. Churchill, Oded Padon, Rahul Sharma, Alex Aiken
2019 A* conf
TASO: optimizing deep learning computation with automatic generation of graph substitutions.
SOSP
Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia, Alex Aiken
2019 — conf
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.
CAV (2)
Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham
2019 J jnl
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.
CoRR
Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham
2018 B conf
Deductive Verification in Decidable Fragments with Ivy.
SAS
Kenneth L. McMillan, Oded Padon
2018 — —
Deductive Verification of Distributed Protocols in First-Order Logic
Oded Padon
2018 B conf
Deductive Verification of Distributed Protocols in First-Order Logic.
FMCAD
Oded Padon
2018 A* conf
Modularity for decidability of deductive verification with applications to distributed systems.
PLDI
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos
2018 J jnl
Reducing liveness to safety in first-order logic.
Proc. ACM Program. Lang.
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2018 B conf
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems.
FMCAD
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2017 — conf
Bounded Quantifier Instantiation for Checking Inductive Invariants.
TACAS (1)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2017 J jnl
Bounded Quantifier Instantiation for Checking Inductive Invariants.
CoRR
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2017 B conf
Conjunctive Abstract Interpretation Using Paramodulation.
VMCAI
Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv
2017 J jnl
Paxos Made EPR: Decidable Reasoning about Distributed Protocols.
CoRR
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
2017 J jnl
Paxos made EPR: decidable reasoning about distributed protocols.
Proc. ACM Program. Lang.
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
2017 B conf
Property Directed Reachability for Proving Absence of Concurrent Modification Errors.
VMCAI
Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham
2017 — conf
RATCOP: Relational Analysis Tool for Concurrent Programs.
Haifa Verification Conference
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
2017 B conf
Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs.
SAS
Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
2016 A* conf
Decidability of inferring inductive invariants.
POPL
Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv
2016 A* conf
Ivy: safety verification by interactive generalization.
PLDI
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
2015 A* conf
Decentralizing SDN Policies.
POPL
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham