Oded Padon

According to our database, Oded Padon authored at least 37 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification.

Neta Elad, Oded Padon, Sharon Shoham

Proc. ACM Program. Lang., January, 2024

2023

Leaf: Modularity for Temporary Sharing in Separation Logic.

Travis Hance, Jon Howell, Oded Padon, Bryan Parno

Proc. ACM Program. Lang., October, 2023

Clover: Closed-Loop Verifiable Code Generation.

Chuyue Sun, Ying Sheng, Oded Padon, Clark W. Barrett

CoRR, 2023

Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version).

Travis Hance, Jon Howell, Oded Padon, Bryan Parno

CoRR, 2023

Quarl: A Learning-Based Quantum Circuit Optimizer.

Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon, Zhihao Jia

CoRR, 2023

Invited Talk: Deductive Verification of Distributed Protocols in Decidable Logics.

Oded Padon

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

2022

Induction duality: primal-dual search for invariants.

Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken

Proc. ACM Program. Lang., 2022

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays.

Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett

Log. Methods Comput. Sci., 2022

Quartz: Superoptimization of Quantum Circuits (Extended Version).

Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia

CoRR, 2022

Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion.

Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Verification of Distributed Protocols: Decidable Modeling and Invariant Inference.

Oded Padon

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

2021

Temporal prophecy for proving temporal properties of infinite-state systems.

Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham

Formal Methods Syst. Des., 2021

Quanto: Optimizing Quantum Circuits with Automatic Generation of Circuit Identities.

Jessica Pointing, Oded Padon, Zhihao Jia, Henry Ma, Auguste Hirth, Jens Palsberg, Alex Aiken

CoRR, 2021

Adaptive restarts for stochastic synthesis.

Jason R. Koenig, Oded Padon, Alex Aiken

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020

A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs.

Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky

CoRR, 2020

Resources: A Safe Language Abstraction for Money.

Sam Blackshear, David L. Dill, Shaz Qadeer, Clark W. Barrett, John C. Mitchell, Oded Padon, Yoni Zohar

CoRR, 2020

First-order quantified separators.

Jason R. Koenig, Oded Padon, Neil Immerman, Alex Aiken

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Ivy: A Multi-modal Verification Tool for Distributed Algorithms.

Kenneth L. McMillan, Oded Padon

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Bounded Quantifier Instantiation for Checking Inductive Invariants.

Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham

Log. Methods Comput. Sci., 2019

TASO: optimizing deep learning computation with automatic generation of graph substitutions.

Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia, Alex Aiken

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Semantic program alignment for equivalence checking.

Berkeley R. Churchill, Oded Padon, Rahul Sharma, Alex Aiken

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

SPoC: Search-based Pseudocode to Code.

Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, Percy Liang

Proceedings of the Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, 2019

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics.

Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, Sharon Shoham

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Deductive Verification of Distributed Protocols in First-Order Logic

Oded Padon

PhD thesis, 2018

Reducing liveness to safety in first-order logic.

Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham

Proc. ACM Program. Lang., 2018

Deductive Verification in Decidable Fragments with Ivy.

Kenneth L. McMillan, Oded Padon

Proceedings of the Static Analysis - 25th International Symposium, 2018

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

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Deductive Verification of Distributed Protocols in First-Order Logic.

Oded Padon

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

2017

Paxos made EPR: decidable reasoning about distributed protocols.

Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham

Proc. ACM Program. Lang., 2017

Conjunctive Abstract Interpretation Using Paramodulation.

Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Property Directed Reachability for Proving Absence of Concurrent Modification Errors.

Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs.

Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky

Proceedings of the Static Analysis - 24th International Symposium, 2017

RATCOP: Relational Analysis Tool for Concurrent Programs.

Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky

Proceedings of the Hardware and Software: Verification and Testing, 2017

2016

Decidability of inferring inductive invariants.

Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Ivy: safety verification by interactive generalization.

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

2015

Decentralizing SDN Policies.

Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015