| Reluplex: An efficient SMT solver for verifying deep neural networks G Katz, C Barrett, DL Dill, K Julian, MJ Kochenderfer International conference on computer aided verification, 97-117, 2017 | 2803 | 2017 |
| Satisfiability Modulo Theories C Barrett, R Sebastiani, SA Seshia, C Tinelli Handbook of Satisfiability 185, 825-885, 2009 | 2427* | 2009 |
| Satisfiability Modulo Theories C Barrett, C Tinelli Handbook of Model Checking, 305-343, 2018 | 2386 | 2018 |
| CVC4 C Barrett, C Conway, M Deters, L Hadarean, D Jovanović, T King, ... Computer aided verification, 171-177, 2011 | 2265 | 2011 |
| The SMT-LIB standard: Version 2.0 C Barrett, A Stump, C Tinelli Proceedings of the 8th international workshop on satisfiability modulo …, 2010 | 1743 | 2010 |
| The satisfiability modulo theories library (SMT-LIB) C Barrett, A Stump, C Tinelli SMT-LIB. org 15, 18-52, 2010 | 937* | 2010 |
| The marabou framework for verification and analysis of deep neural networks G Katz, DA Huang, D Ibeling, K Julian, C Lazarus, R Lim, P Shah, ... International conference on computer aided verification, 443-452, 2019 | 857 | 2019 |
| 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 | 852 | 2022 |
| H2o: Heavy-hitter oracle for efficient generative inference of large language models Z Zhang, Y Sheng, T Zhou, T Chen, L Zheng, R Cai, Z Song, Y Tian, C Ré, ... Advances in Neural Information Processing Systems 36, 34661-34710, 2023 | 772 | 2023 |
| Flexgen: High-throughput generative inference of large language models with a single gpu Y Sheng, L Zheng, B Yuan, Z Li, M Ryabinin, B Chen, P Liang, C Ré, ... International Conference on Machine Learning, 31094-31116, 2023 | 697 | 2023 |
| Algorithms for verifying deep neural networks C Liu, T Arnon, C Lazarus, C Strong, C Barrett, MJ Kochenderfer Foundations and Trends in Optimization 4 (3-4), 244-404, 2021 | 585 | 2021 |
| CVC Lite: A new implementation of the cooperating validity checker: Category B C Barrett, S Berezin International Conference on Computer Aided Verification, 515-518, 2004 | 403 | 2004 |
| Sglang: Efficient execution of structured language model programs L Zheng, L Yin, Z Xie, CL Sun, J Huang, CH Yu, S Cao, C Kozyrakis, ... Advances in neural information processing systems 37, 62557-62583, 2024 | 373 | 2024 |
| CVC: A cooperating validity checker A Stump, CW Barrett, DL Dill International Conference on Computer Aided Verification, 500-504, 2002 | 289 | 2002 |
| Validity checking for combinations of theories with equality C Barrett, D Dill, J Levitt International Conference on Formal Methods in Computer-Aided Design, 187-201, 1996 | 277 | 1996 |
| A decision procedure for an extensional theory of arrays A Stump, CW Barrett, DL Dill, J Levitt Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, 29-37, 2001 | 239 | 2001 |
| Checking satisfiability of first-order formulas by incremental translation to SAT CW Barrett, DL Dill, A Stump International Conference on Computer Aided Verification, 236-249, 2002 | 230 | 2002 |
| A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions T Liang, A Reynolds, C Tinelli, C Barrett, M Deters International Conference on Computer Aided Verification, 646-662, 2014 | 193 | 2014 |
| A decision procedure for bit-vector arithmetic CW Barrett, DL Dill, JR Levitt Proceedings of the 35th Annual Design Automation Conference, 522-527, 1998 | 193 | 1998 |
| Counterexample-guided quantifier instantiation for synthesis in SMT A Reynolds, M Deters, V Kuncak, C Tinelli, C Barrett International Conference on Computer Aided Verification, 198-216, 2015 | 189 | 2015 |
Cesare TinelliProfessor of Computer Science, The University of IowaVerified email at uiowa.edu
