Следене
Oded Padon
Oded Padon
VMware Research
Потвърден имейл адрес: vmware.com - Начална страница
Заглавие
Позовавания
Позовавания
Година
Ivy: safety verification by interactive generalization
O Padon, KL McMillan, A Panda, M Sagiv, S Shoham
PLDI, 614-630, 2016
2322016
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
2192019
Paxos made EPR: decidable reasoning about distributed protocols
O Padon, G Losa, M Sagiv, S Shoham
OOPSLA, 108, 2017
1122017
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
1072019
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
862019
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
562018
Reducing liveness to safety in first-order logic
O Padon, J Hoenicke, G Losa, A Podelski, M Sagiv, S Shoham
POPL, 26, 2018
462018
Decidability of inferring inductive invariants
O Padon, N Immerman, S Shoham, A Karbyshev, M Sagiv
POPL, 217-231, 2016
442016
Ivy: a multi-modal verification tool for distributed algorithms
KL McMillan, O Padon
Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020
432020
Decentralizing SDN policies
O Padon, N Immerman, A Karbyshev, O Lahav, M Sagiv, S Shoham
POPL, 663-676, 2015
362015
First-order quantified separators
JR Koenig, O Padon, N Immerman, A Aiken
Proceedings of the 41st ACM SIGPLAN conference on programming language …, 2020
312020
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
292019
Deductive Verification in Decidable Fragments with Ivy
KL McMillan, O Padon
SAS, 43-55, 2018
252018
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
242022
Bounded quantifier instantiation for checking inductive invariants
YMY Feldman, O Padon, N Immerman, M Sagiv, S Shoham
TACAS, 76-95, 2017
202017
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
172021
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
152022
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
122022
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
122021
Deductive verification of distributed protocols in first-order logic
O Padon
2018 Formal Methods in Computer Aided Design (FMCAD), 1-1, 2018
92018
Системата не може да изпълни операцията сега. Опитайте отново по-късно.
Статии 1–20