Follow
Oded Padon
Oded Padon
VMware Research
Verified email at vmware.com - Homepage
Title
Cited by
Cited by
Year
TASO: optimizing deep learning computation with automatic generation of graph substitutions
Z Jia, O Padon, J Thomas, T Warszawski, M Zaharia, A Aiken
Proceedings of the 27th ACM Symposium on Operating Systems Principles, 47-62, 2019
2812019
Ivy: safety verification by interactive generalization
O Padon, KL McMillan, A Panda, M Sagiv, S Shoham
PLDI, 614-630, 2016
2622016
Spoc: Search-based pseudocode to code
S Kulal, P Pasupat, K Chandra, M Lee, O Padon, A Aiken, P Liang
Advances in Neural Information Processing Systems 32 (NeurIPS 2019), 2019
1882019
Paxos made EPR: decidable reasoning about distributed protocols
O Padon, G Losa, M Sagiv, S Shoham
OOPSLA, 108, 2017
1262017
Semantic program alignment for equivalence checking
B Churchill, O Padon, R Sharma, A Aiken
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019
1032019
Modularity for decidability of deductive verification with applications to distributed systems
M Taube, G Losa, KL McMillan, O Padon, M Sagiv, S Shoham, JR Wilcox, ...
PLDI, 662-677, 2018
722018
Ivy: A multi-modal verification tool for distributed algorithms
KL McMillan, O Padon
Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020
612020
Reducing liveness to safety in first-order logic
O Padon, J Hoenicke, G Losa, A Podelski, M Sagiv, S Shoham
POPL, 26, 2018
582018
Quartz: superoptimization of quantum circuits
M Xu, Z Li, O Padon, S Lin, J Pointing, A Hirth, H Ma, J Palsberg, A Aiken, ...
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022
482022
Decidability of inferring inductive invariants
O Padon, N Immerman, S Shoham, A Karbyshev, M Sagiv
POPL, 217-231, 2016
482016
First-order quantified separators
JR Koenig, O Padon, N Immerman, A Aiken
Proceedings of the 41st ACM SIGPLAN conference on programming language …, 2020
392020
Decentralizing SDN policies
O Padon, N Immerman, A Karbyshev, O Lahav, M Sagiv, S Shoham
POPL, 663-676, 2015
382015
Verification of threshold-based distributed algorithms by decomposition to decidable logics
I Berkovits, M Lazić, G Losa, O Padon, S Shoham
Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019
372019
Deductive Verification in Decidable Fragments with Ivy
KL McMillan, O Padon
SAS, 43-55, 2018
272018
Induction Duality: Primal-Dual Search for Invariants
O Padon, JR Wilcox, JR Koenig, KL McMillan, A Aiken
Proc. ACM Program. Lang. 6 (POPL), 50:1--50:29, 2022
232022
Bounded quantifier instantiation for checking inductive invariants
YMY Feldman, O Padon, N Immerman, M Sagiv, S Shoham
TACAS, 76-95, 2017
232017
Quanto: Optimizing quantum circuits with automatic generation of circuit identities
J Pointing, O Padon, Z Jia, H Ma, A Hirth, J Palsberg, A Aiken
Quantum Science and Technology 9 (4), 045009, 2024
222024
Counterexample-guided prophecy for model checking modulo the theory of arrays
M Mann, A Irfan, A Griggio, O Padon, C Barrett
Logical Methods in Computer Science 18, 2022
192022
Temporal prophecy for proving temporal properties of infinite-state systems
O Padon, J Hoenicke, KL McMillan, A Podelski, M Sagiv, S Shoham
Formal Methods in System Design 57, 246-269, 2021
172021
Deductive verification of distributed protocols in first-order logic
O Padon
2018 Formal Methods in Computer Aided Design (FMCAD), 1-1, 2018
162018
The system can't perform the operation now. Try again later.
Articles 1–20