Oded Padon
Oded Padon
VMware Research
Bestätigte E-Mail-Adresse bei - Startseite
Zitiert von
Zitiert von
Ivy: safety verification by interactive generalization
O Padon, KL McMillan, A Panda, M Sagiv, S Shoham
PLDI, 614-630, 2016
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
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
Paxos made EPR: decidable reasoning about distributed protocols
O Padon, G Losa, M Sagiv, S Shoham
OOPSLA, 108, 2017
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
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
Reducing liveness to safety in first-order logic
O Padon, J Hoenicke, G Losa, A Podelski, M Sagiv, S Shoham
POPL, 26, 2018
Ivy: A multi-modal verification tool for distributed algorithms
KL McMillan, O Padon
Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020
Decidability of inferring inductive invariants
O Padon, N Immerman, S Shoham, A Karbyshev, M Sagiv
POPL, 217-231, 2016
Decentralizing SDN policies
O Padon, N Immerman, A Karbyshev, O Lahav, M Sagiv, S Shoham
POPL, 663-676, 2015
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
First-order quantified separators
JR Koenig, O Padon, N Immerman, A Aiken
Proceedings of the 41st ACM SIGPLAN conference on programming language …, 2020
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
Deductive Verification in Decidable Fragments with Ivy
KL McMillan, O Padon
SAS, 43-55, 2018
Bounded quantifier instantiation for checking inductive invariants
YMY Feldman, O Padon, N Immerman, M Sagiv, S Shoham
TACAS, 76-95, 2017
Quanto: Optimizing quantum circuits with automatic generation of circuit identities
J Pointing, O Padon, Z Jia, H Ma, A Hirth, J Palsberg, A Aiken
arXiv preprint arXiv:2111.11387, 2021
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
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
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
Resources: A safe language abstraction for money
S Blackshear, DL Dill, S Qadeer, CW Barrett, JC Mitchell, O Padon, ...
arXiv preprint arXiv:2004.05106, 2020
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20