| 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 | 313 | 2019 |
| Ivy: safety verification by interactive generalization O Padon, KL McMillan, A Panda, M Sagiv, S Shoham PLDI, 614-630, 2016 | 275 | 2016 |
| 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 | 227 | 2019 |
| Paxos made EPR: decidable reasoning about distributed protocols O Padon, G Losa, M Sagiv, S Shoham OOPSLA, 108, 2017 | 133 | 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 | 112 | 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 | 77 | 2018 |
| Ivy: A multi-modal verification tool for distributed algorithms KL McMillan, O Padon Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020 | 66 | 2020 |
| Reducing liveness to safety in first-order logic O Padon, J Hoenicke, G Losa, A Podelski, M Sagiv, S Shoham POPL, 26, 2018 | 62 | 2018 |
| 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 | 61 | 2022 |
| Decidability of inferring inductive invariants O Padon, N Immerman, S Shoham, A Karbyshev, M Sagiv POPL, 217-231, 2016 | 49 | 2016 |
| First-order quantified separators JR Koenig, O Padon, N Immerman, A Aiken Proceedings of the 41st ACM SIGPLAN conference on programming language …, 2020 | 44 | 2020 |
| Decentralizing SDN policies O Padon, N Immerman, A Karbyshev, O Lahav, M Sagiv, S Shoham POPL, 663-676, 2015 | 39 | 2015 |
| 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 | 37 | 2019 |
| Clover: Closed-Loop Verifiable Code Generation C Sun, Y Sheng, O Padon, C Barrett International Symposium on AI Verification, 134-155, 2024 | 30 | 2024 |
| Deductive Verification in Decidable Fragments with Ivy KL McMillan, O Padon SAS, 43-55, 2018 | 28 | 2018 |
| Bounded quantifier instantiation for checking inductive invariants YMY Feldman, O Padon, N Immerman, M Sagiv, S Shoham TACAS, 76-95, 2017 | 27 | 2017 |
| 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 | 26 | 2022 |
| 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 | 24 | 2024 |
| 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 | 21 | 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 | 19 | 2022 |
Sharon ShohamTel Aviv UniversityVerified email at tauex.tau.ac.il