| cvc5: A versatile and industrial-strength SMT solver H Barbosa, C Barrett, M Brain, G Kremer, H Lachnitt, M Mann, ... International Conference on Tools and Algorithms for the Construction and …, 2022 | 447 | 2022 |
| Online detection of effectively callback free objects with applications to smart contracts S Grossman, I Abraham, G Golan-Gueta, Y Michalevsky, N Rinetzky, ... Proceedings of the ACM on Programming Languages 2 (POPL), 1-28, 2017 | 244 | 2017 |
| The move prover JE Zhong, K Cheang, S Qadeer, W Grieskamp, S Blackshear, J Park, ... Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020 | 30 | 2020 |
| Flexible proof production in an industrial-strength SMT solver H Barbosa, A Reynolds, G Kremer, H Lachnitt, A Niemetz, A Nötzli, ... International Joint Conference on Automated Reasoning, 15-35, 2022 | 26 | 2022 |
| Towards bit-width-independent proofs in SMT solvers A Niemetz, M Preiner, A Reynolds, Y Zohar, C Barrett, C Tinelli Automated Deduction–CADE 27: 27th International Conference on Automated …, 2019 | 24 | 2019 |
| Rexpansions of nondeterministic matrices and their applications in nonclassical logics A Avron, Y Zohar The Review of Symbolic Logic 12 (1), 173-200, 2019 | 20 | 2019 |
| SMT-switch: a solver-agnostic C++ API for SMT solving M Mann, A Wilson, Y Zohar, L Stuntz, A Irfan, K Brown, C Donovick, ... International Conference on Theory and Applications of Satisfiability …, 2021 | 18 | 2021 |
| SAT-based decision procedure for analytic pure sequent calculi O Lahav, Y Zohar International Joint Conference on Automated Reasoning, 76-90, 2014 | 18 | 2014 |
| Sequent systems for negative modalities O Lahav, J Marcos, Y Zohar Logica Universalis 11, 345-382, 2017 | 16 | 2017 |
| Bit-precise reasoning via int-blasting Y Zohar, A Irfan, M Mann, A Niemetz, A Nötzli, M Preiner, A Reynolds, ... International Conference on Verification, Model Checking, and Abstract …, 2022 | 14 | 2022 |
| 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 | 13 | 2020 |
| Yet another paradefinite logic: The role of conflation N Kamide, Y Zohar Logic Journal of the IGPL 27 (1), 93-117, 2019 | 12 | 2019 |
| On the construction of analytic sequent calculi for sub-classical logics O Lahav, Y Zohar International Workshop on Logic, Language, Information, and Computation, 206-220, 2014 | 11 | 2014 |
| Towards satisfiability modulo parametric bit-vectors A Niemetz, M Preiner, A Reynolds, Y Zohar, C Barrett, C Tinelli Journal of Automated Reasoning 65 (7), 1001-1025, 2021 | 9 | 2021 |
| Politeness for the theory of algebraic datatypes Y Sheng, Y Zohar, C Ringeissen, J Lange, P Fontaine, C Barrett International Joint Conference on Automated Reasoning, 238-255, 2020 | 9 | 2020 |
| DRAT-based bit-vector proofs in CVC4 A Ozdemir, A Niemetz, M Preiner, Y Zohar, C Barrett Theory and Applications of Satisfiability Testing–SAT 2019: 22nd …, 2019 | 8 | 2019 |
| Effective semantics for the modal logics K and KT via non-deterministic matrices O Lahav, Y Zohar International Joint Conference on Automated Reasoning, 468-485, 2022 | 7 | 2022 |
| Politeness and stable infiniteness: stronger together CB Reynolds, C Tinelli Automated Deduction–CADE 28, 148, 2021 | 7 | 2021 |
| Generating and exploiting automated reasoning proof certificates H Barbosa, C Barrett, B Cook, B Dutertre, G Kremer, H Lachnitt, A Niemetz, ... Communications of the ACM 66 (10), 86-95, 2023 | 6 | 2023 |
| Reasoning about vectors using an SMT theory of sequences Y Sheng, A Nötzli, A Reynolds, Y Zohar, D Dill, W Grieskamp, J Park, ... International Joint Conference on Automated Reasoning, 125-143, 2022 | 6 | 2022 |
Clark BarrettStanford UniversityVerified email at cs.stanford.edu
