Oded Padon

Publication Activity (10 Years)

Years Active: 2014-2024
Publications (10 Years): 53

Top Topics

Abstract Interpretation

Quantifier Elimination

Distributed Systems

Top Venues

Proc. ACM Program. Lang.

Publications

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