Bio

Clark Barrett is a Professor (Research) of Computer Science at Stanford University. Before coming to Stanford in 2016, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. His expertise is in automated reasoning and its applications. His PhD dissertation (Stanford, 2003) introduced a novel automated reasoning technique now known as Satisfiability Modulo Theories (SMT). He was an early pioneer in formal hardware verification as part of 0-in Design Automation (now part of Siemens/Mentor Graphics), where he helped build one of the first industrially successful assertion-based verification tool-sets for hardware. More recently, he has also pioneered techniques for applying formal methods to neural networks. His current work focuses on the development and application of automated reasoning techniques to improve reliability and security of software, hardware, and machine learning systems. He is the director of the Stanford Center for Automated Reasoning (Centaur) and co-director of the Stanford Center for AI Safety. He is an ACM Distinguished Scientist and a winner of the Computer Aided Verification (CAV) award in 2021 and 2024.

Academic Appointments

Administrative Appointments

  • Amazon Scholar, Amazon Web Services (2023 - Present)
  • Director, Center for Automated Reasoning (Centaur) (2021 - Present)
  • Co-director, Center for AI Safety (2019 - Present)
  • Visiting Scientist, Google (2015 - 2017)

Honors & Awards

  • CAV Award for pioneering the application of formal methods to neural networks., Computer Aided Verification conference (CAV) (2024)
  • Best SCP Tool Paper for "cvc5: A Versatile and Industrial-Strength SMT Solver", Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2022)
  • CAV Award for pioneering contributions to ... theory and practice of satisfiability modulo theories, Computer Aided Verification conference (CAV) (2021)
  • Test of Time award for "A Decision Procedure for an Extensional Theory of Arrays", Logic in Computer Science (LICS) (2021)
  • Best Paper for "Politeness for the Theory of Algebraic Datatypes", International Joint Conference on Automated Reasoning (IJCAR) (2020)
  • First place (CoSA2 model checker), Hardware Model Checking Competition (HWCC) (2019)
  • Best Short Paper for "p4pktgen: Automated Test-Case Generation for P4 Programs", Symposium on Software Defined Networking Research (SOSR) (2018)
  • Distinguished Artifact Award for "EMME: A Formal Tool for ECMAScript Memory Model Evaluation", Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2018)
  • Best Paper for "Lazy Proofs for DPLL(T)-Based SMT Solvers", International Conference on Formal Methods in Computer-Aided Design (FMCAD) (2016)
  • Best Paper for "A Structured Approach to Post-Silicon Validation and Debug using Symbolic QED", IEEE International Test Conference (ITC) (2015)
  • Distinguished Scientist, ACM (2014)
  • HVC Award, Haifa Verification Conference (2010)
  • Software Quality Innovation Award, IBM (2008)
  • CAREER award, National Science Foundation (2007)
  • Best Paper for "A Decision Procedure for Bit-vector Arithmetic", Design Automation Conference (DAC) (1998)

Professional Education

  • Ph.D., Stanford University, Computer Science (2003)

Patents

  • Subhasish Mitra, Clark Barrett, David Lin, Eshan Singh. "United States Patent 10528448 Post-silicon Validation and Debug using Symbolic Quick Error Detection", The Board of Trustees of the Leland Stanford Junior University (Palo Alto, CA, US); New York University (New York, NY, US), Jan 7, 2020

Contact

  • Academic
    barrettc@stanford.edu
    University - Faculty Department: Computer Science Position: Professor (Research)
    • Department of Computer Science
    • Gates 488
    • Stanford University
    • Stanford,  California  94305 

Additional Info

Links

Current Research and Scholarly Interests

In an increasingly automated and networked world, one of the most pressing challenges we face is ensuring the security and dependability of hardware, software, and AI systems. Formal techniques (based on mathematical logic and automated reasoning) are among the most powerful tools available for finding difficult bugs and ensuring correctness. Unfortunately, formal methods today either require extensive manual effort or are severely limited in their scope or scalability. My research vision is to develop general-purpose, automated, and scalable formal techniques, with the aim of providing a sound and practical foundation for reliable computer systems.

Projects

  • cvc5, Stanford University (5/6/2021 - Present)

    A versatile and industrial-strength open-source SMT solver

    Location

    Stanford, CA

    Collaborators

    • C Tinelli, Professor, University of Iowa
    • Haniel Barbosa, Assistant Professor, Universidade Federal de Minas Gerais
    • Yoni Zohar, Faculty, Bar Ilan University

    For More Information:

  • Marabou, Stanford University

    A tool for formal verification of neural networks

    Location

    Stanford, CA

    Collaborators

    • Guy Katz, Assistant Professor, Hebrew University

    For More Information:

  • Pono, Stanford University

    SMT-based model checker

    Location

    Stanford, CA

2024-25 Courses

Stanford Advisees

All Publications

  • Towards Efficient Verification of Quantized Neural Networks Huang, P., Wu, H., Yang, Y., Daukantas, I., Wu, M., Zhang, Y., Barrett, C., Wooldridge, M., Dy, J., Natarajan, S. ASSOC ADVANCEMENT ARTIFICIAL INTELLIGENCE. 2024: 21152-21160

    View details for Web of Science ID 001239984900029

  • Clover: Closed-Loop Verifiable Code Generation Sun, C., Sheng, Y., Padon, O., Barrett, C., Avni, G., Giacobbe, M., Johnson, T. T., Katz, G., Lukina, A., Narodytska, N., Schilling, C. SPRINGER INTERNATIONAL PUBLISHING AG. 2024: 134-155

    View details for DOI 10.1007/978-3-031-65112-0_7

    View details for Web of Science ID 001312952000007

  • Parallel Verification for δ-Equivalence of Neural Network Quantization Huang, P., Yang, Y., Wu, H., Daukantas, I., Wu, M., Jia, F., Barrett, C., Avni, G., Giacobbe, M., Johnson, T. T., Katz, G., Lukina, A., Narodytska, N., Schilling, C. SPRINGER INTERNATIONAL PUBLISHING AG. 2024: 78-99

    View details for DOI 10.1007/978-3-031-65112-0_4

    View details for Web of Science ID 001312952000004

  • Split Grobner Bases for Satisfiability Modulo Finite Fields Ozdemir, A., Pailoor, S., Bassa, A., Ferles, K., Barrett, C., Dillig, I., Gurfinkel, A., Ganesh SPRINGER INTERNATIONAL PUBLISHING AG. 2024: 3-25

    View details for DOI 10.1007/978-3-031-65627-9_1

    View details for Web of Science ID 001307887200001

  • IsaRARE: Automatic Verification of SMT Rewrites in Isabelle/HOL Lachnitt, H., Fleury, M., Aniva, L., Reynolds, A., Barbosa, H., Notzli, A., Barrett, C., Tinelli, C., Finkbeiner, B., Kovacs, L. SPRINGER INTERNATIONAL PUBLISHING AG. 2024: 311-330

    View details for DOI 10.1007/978-3-031-57246-3_17

    View details for Web of Science ID 001284177100017

  • Generalized Optimization Modulo Theories Tsiskaridze, N., Barrett, C., Tinelli, C., Benzmuller, C., Heule, M. J., Schmidt, R. A. SPRINGER INTERNATIONAL PUBLISHING AG. 2024: 458-479

    View details for DOI 10.1007/978-3-031-63498-7_27

    View details for Web of Science ID 001273489700027

  • Marabou 2.0: A Versatile Formal Analyzer of Neural Networks Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C., Ganesh, Gurfinkel, A. SPRINGER INTERNATIONAL PUBLISHING AG. 2024: 249-264

    View details for DOI 10.1007/978-3-031-65630-9_13

    View details for Web of Science ID 001307890400013

  • Combining Stable Infiniteness and (Strong) Politeness JOURNAL OF AUTOMATED REASONING Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C., Tinelli, C. 2023; 67 (4)

    View details for DOI 10.1007/s10817-023-09684-0

    View details for Web of Science ID 001072387000001

  • Generating and Exploiting Automated Reasoning Proof Certificates COMMUNICATIONS OF THE ACM Barbosa, H., Barrett, C., Cook, B., Dutertre, B., Kremer, G., Lachnitt, H., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Tinelli, C., Zohar, Y. 2023; 66 (10): 86-95

    View details for DOI 10.1145/3587692

    View details for Web of Science ID 001075786500018

  • Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences JOURNAL OF AUTOMATED REASONING Sheng, Y., Notzli, A., Reynolds, A., Zohar, Y., Dill, D., Grieskamp, W., Park, J., Qadeer, S., Barrett, C., Tinelli, C. 2023; 67 (3)

    View details for DOI 10.1007/s10817-023-09682-2

    View details for Web of Science ID 001067178200001

  • Synthesising Programs with Non-trivial Constants. Journal of automated reasoning Abate, A., Barbosa, H., Barrett, C., David, C., Kesseli, P., Kroening, D., Polgreen, E., Reynolds, A., Tinelli, C. 2023; 67 (2): 19

    Abstract

    Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. While useful in general, such syntactic restrictions provide little help for the generation of programs that contain non-trivial constants, unless the user is able to provide the constants in advance. This is a fundamentally difficult task for state-of-the-art synthesisers. We propose a new approach to the synthesis of programs with non-trivial constants that combines the strengths of a counterexample-guided inductive synthesiser with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T), where T is a first-order theory. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate the practical value of CEGIS(T) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(T) within the mature synthesiser CVC4 and show that CEGIS(T) improves CVC4's results.

    View details for DOI 10.1007/s10817-023-09664-4

    View details for PubMedID 37193313

    View details for PubMedCentralID PMC10182957

  • Formal Verification of Bit-Vector Invertibility Conditions in Coq Ekici, B., Viswanathan, A., Zohar, Y., Tinelli, C., Barrett, C., Sattler, U., Suda, M. SPRINGER INTERNATIONAL PUBLISHING AG. 2023: 41-59

    View details for DOI 10.1007/978-3-031-43369-6_3

    View details for Web of Science ID 001156327100003

  • Satisfiability Modulo Finite Fields Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C., Enea, C., Lal, A. SPRINGER INTERNATIONAL PUBLISHING AG. 2023: 163-186

    View details for DOI 10.1007/978-3-031-37703-7_8

    View details for Web of Science ID 001310804800008

  • Bounded Verification for Finite-Field-Blasting In a Compiler for Zero Knowledge Proofs Ozdemir, A., Wahby, R. S., Brown, F., Barrett, C., Enea, C., Lal, A. SPRINGER INTERNATIONAL PUBLISHING AG. 2023: 154-175

    View details for DOI 10.1007/978-3-031-37709-9_8

    View details for Web of Science ID 001310805600008

  • On Optimal Caching and Model Multiplexing for Large Model Inference Zhu, B., Sheng, Y., Zheng, L., Barrett, C., Jordan, M. I., Jiao, J., Oh, A., Neumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. NEURAL INFORMATION PROCESSING SYSTEMS (NIPS). 2023

    View details for Web of Science ID 001229826605009

  • H<sub>2</sub>O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models Zhang, Z., Sheng, Y., Zhou, T., Chen, T., Zheng, L., Cai, R., Song, Z., Tian, Y., Re, C., Barrett, C., Wang, Z., Chen, B., Oh, A., Neumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. NEURAL INFORMATION PROCESSING SYSTEMS (NIPS). 2023

    View details for Web of Science ID 001224281503036

  • <i>Soy</i>: An Efficient MILP Solver for Piecewise-Affine Systems Wu, H., Wu, M., Sadigh, D., Barrett, C., IEEE IEEE. 2023: 6281-6288

    View details for DOI 10.1109/IROS55552.2023.10342011

    View details for Web of Science ID 001136907800122

  • VERIX: Towards Verified Explainability of Deep Neural Networks Wu, M., Wu, H., Barrett, C., Oh, A., Neumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. NEURAL INFORMATION PROCESSING SYSTEMS (NIPS). 2023

    View details for Web of Science ID 001230083404006

  • Toward Certified Robustness Against Real-World Distribution Shifts Wu, H., Tagomori, T., Robey, A., Yang, F., Matni, N., Pappas, G., Hassani, H., Pasareanu, C., Barrett, C., IEEE IEEE COMPUTER SOC. 2023: 537-553

    View details for DOI 10.1109/SaTML54575.2023.00042

    View details for Web of Science ID 001012311500032

  • AHA: An Agile Approach to the Design of Coarse-Grained Reconfigurable Accelerators and Compilers ACM Transactions on Embedded Computing Systems Koul, K., Melchert, J., Sreedhar, K., Truong, L., Nyengele, G., Zhang, K., Liu, Q., Setter, J., Chen, P., Mei, Y., Strange, M., Daly, R., Donovick, C., Carsello, A., Kong, T., Feng, K., Huff, D., Nayak, A., Setaluri, R., Thomas, J., Bhagdikar, N., Durst, D., Myers, Z., Tsiskaridze, N., Richardson, S., et al 2023; 22 (2)

    View details for DOI 10.1145/3534933

  • G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators Chattopadhyay, S., Devarajegowda, K., Zhao, B., Lonsing, F., D'Agostino, B. A., Vavelidou, I., Bhatt, V. D., Prebeck, S., Ecker, W., Trippel, C., Barrett, C., Mitra, S., IEEE IEEE. 2023

    View details for DOI 10.1109/DAC56929.2023.10247903

    View details for Web of Science ID 001073487300211

  • Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness Toledo, G. V., Zohar, Y., Barrett, C., Pientka, B., Tinelli, C. SPRINGER INTERNATIONAL PUBLISHING AG. 2023: 522-541

    View details for DOI 10.1007/978-3-031-38499-8_30

    View details for Web of Science ID 001156342400028

  • Combining Finite Combination Properties: Finite Models and Busy Beavers Toledo, G. V., Zohar, Y., Barrett, C., Sattler, U., Suda, M. SPRINGER INTERNATIONAL PUBLISHING AG. 2023: 159-175

    View details for DOI 10.1007/978-3-031-43369-6_9

    View details for Web of Science ID 001156327100009

  • Scalable Verification of GNN-Based Job Schedulers PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL Wu, H., Barrett, C., Sharif, M., Narodytska, N., Singh, G. 2022; 6 (OOPSLA)

    View details for DOI 10.1145/3563325

    View details for Web of Science ID 001083750200039

  • Polite Combination of Algebraic Datatypes JOURNAL OF AUTOMATED REASONING Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C. 2022

    View details for DOI 10.1007/s10817-022-09625-3

    View details for Web of Science ID 000791156700001

  • Even Faster Conflicts and Lazier Reductions for String Solvers Notzli, A., Reynolds, A., Barbosa, H., Barrett, C., Tinelli, C., Shoham, S., Vizel, Y. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 205-226

    View details for DOI 10.1007/978-3-031-13188-2_11

    View details for Web of Science ID 000870310500011

  • Neural Network Verification with Proof Production Isac, O., Barrett, C., Zhang, M., Katz, G., Griggio, A., Rungta, N. TU Wien Acad Press. 2022: 38-48

    View details for DOI 10.34727/2022/isbn.978-3-85448-053-2_9

    View details for Web of Science ID 001062691400009

  • Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language Notzli, A., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C., Griggio, A., Rungta, N. TU Wien Acad Press. 2022: 65-74

    View details for DOI 10.34727/2022/isbn.978-3-85448-053-2_12

    View details for Web of Science ID 001062691400012

  • Bit-Precise Reasoning via Int-Blasting Zohar, Y., Irfan, A., Mann, M., Niemetz, A., Notzli, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C., Finkbeiner, B., Wies, T. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 496-518

    View details for DOI 10.1007/978-3-030-94583-1_24

    View details for Web of Science ID 001059208500024

  • <i>Proof</i>-<i>Stitch</i>: Proof Combination for Divide-and-Conquer SAT Solvers Nair, A., Chattopadhyay, S., Wu, H., Ozdemir, A., Barrett, C., Griggio, A., Rungta, N. TU Wien Acad Press. 2022: 84-88

    View details for DOI 10.34727/2022/isbn.978-3-85448-053-2_14

    View details for Web of Science ID 001062691400014

  • On Optimizing Back-Substitution Methods for Neural Network Verification Zelazny, T., Wu, H., Barrett, C., Katz, G., Griggio, A., Rungta, N. TU Wien Acad Press. 2022: 17-26

    View details for DOI 10.34727/2022/isbn.978-3-85448-053-2_7

    View details for Web of Science ID 001062691400007

  • Synthesizing Instruction Selection Rewrite Rules from RTL using SMT Daly, R., Donovick, C., Melchert, J., Setaluri, R., Bullock, N., Raina, P., Barrett, C., Hanrahan, P., Griggio, A., Rungta, N. TU Wien Acad Press. 2022: 139-150

    View details for DOI 10.34727/2022/isbn.978-3-85448-053-2_20

    View details for Web of Science ID 001062691400020

  • Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description) Kremer, G., Reynolds, A., Barrett, C., Tinelli, C., Blanchette, J., Kovacs, L., Pattinson, D. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 95-105

    View details for DOI 10.1007/978-3-031-10769-6_7

    View details for Web of Science ID 000876376400007

  • Efficient Neural Network Analysis with Sum-of-Infeasibilities Wu, H., Zeljic, A., Katz, G., Barrett, C., Fisman, D., Rosu, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 143-163

    View details for DOI 10.1007/978-3-030-99524-9_8

    View details for Web of Science ID 000782396700008

  • cvc5: A Versatile and Industrial-Strength SMT Solver Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y., Fisman, D., Rosu, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 415-442

    View details for DOI 10.1007/978-3-030-99524-9_24

    View details for Web of Science ID 000782396700024

  • Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers Niemetz, A., Preiner, M., Barrett, C., Shoham, S., Vizel, Y. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 92-106

    View details for DOI 10.1007/978-3-031-13188-2_5

    View details for Web of Science ID 000870310500005

  • Flexible Proof Production in an Industrial-Strength SMT Solver Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Barrett, C., Blanchette, J., Kovacs, L., Pattinson, D. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 15-35

    View details for DOI 10.1007/978-3-031-10769-6_3

    View details for Web of Science ID 000876376400003

  • Reasoning About Vectors Using an SMT Theory of Sequences Sheng, Y., Notzli, A., Reynolds, A., Zohar, Y., Dill, D., Grieskamp, W., Park, J., Qadeer, S., Barrett, C., Tinelli, C., Blanchette, J., Kovacs, L., Pattinson, D. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 125-143

    View details for DOI 10.1007/978-3-031-10769-6_9

    View details for Web of Science ID 000876376400009

  • Global optimization of objective functions represented by ReLU networks MACHINE LEARNING Strong, C. A., Wu, H., Zeljic, A., Julian, K. D., Katz, G., Barrett, C., Kochenderfer, M. J. 2021

    View details for DOI 10.1007/s10994-021-06050-2

    View details for Web of Science ID 000709232800001

  • Reluplex: a calculus for reasoning about deep neural networks FORMAL METHODS IN SYSTEM DESIGN Katz, G., Barrett, C., Dill, D. L., Julian, K., Kochenderfer, M. J. 2021

    View details for DOI 10.1007/s10703-021-00363-7

    View details for Web of Science ID 000668847200001

  • Towards Satisfiability Modulo Parametric Bit-vectors JOURNAL OF AUTOMATED REASONING Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C. 2021

    View details for DOI 10.1007/s10817-021-09598-9

    View details for Web of Science ID 000663269800001

  • On solving quantified bit-vector constraints using invertibility conditions FORMAL METHODS IN SYSTEM DESIGN Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C. 2021

    View details for DOI 10.1007/s10703-020-00359-9

    View details for Web of Science ID 000608679200001

  • Pono: A Flexible and Extensible SMT-Based Model Checker Mann, M., Irfan, A., Lonsing, F., Yang, Y., Zhang, H., Brown, K., Gupta, A., Barrett, C., Silva, A., Leino, K. R. SPRINGER INTERNATIONAL PUBLISHING AG. 2021: 461-474

    View details for DOI 10.1007/978-3-030-81688-9_22

    View details for Web of Science ID 000693429500022

  • DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers Paterson, C., Wu, H., Grese, J., Calinescu, R., Pasareanu, C. S., Barrett, C., Habli, Sujan, M., Bitsch, F. SPRINGER INTERNATIONAL PUBLISHING AG. 2021: 3-17

    View details for DOI 10.1007/978-3-030-83903-1_5

    View details for Web of Science ID 000696703000001

  • COUNTEREXAMPLE-GUIDED PROPHECY FOR MODEL CHECKING MODULO THE THEORY OF ARRAYS LOGICAL METHODS IN COMPUTER SCIENCE Mann, M., Irfan, A., Griggio, A., Padon, O., Barrett, C. 2021; 18 (3)

    View details for DOI 10.46298/LMCS-18(3:26)2022

    View details for Web of Science ID 000860394200002

  • Smt-Switch: A Solver-Agnostic C plus plus API for SMT Solving Mann, M., Wilson, A., Zohar, Y., Stuntz, L., Irfan, A., Brown, K., Donovick, C., Guman, A., Tinelli, C., Barrett, C., Li, C. M., Manya, F. SPRINGER INTERNATIONAL PUBLISHING AG. 2021: 377-386

    View details for DOI 10.1007/978-3-030-80223-3_26

    View details for Web of Science ID 000709570900026

  • Politeness and Stable Infiniteness: Stronger Together Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C., Tinelli, C., Platzer, A., Sutcliffe, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2021: 148-165

    View details for DOI 10.1007/978-3-030-79876-5_9

    View details for Web of Science ID 000693448800009

  • The Move Prover Zhong, J., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C., Dill, D. L., Lahiri, S. K., Wang, C. SPRINGER INTERNATIONAL PUBLISHING AG. 2020: 137-150

    View details for DOI 10.1007/978-3-030-53288-8_7

    View details for Web of Science ID 000695276000007

  • Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance Irfan, A., Julian, K. D., Wu, H., Barrett, C., Kochenderfer, M. J., Meng, B., Lopez, J., IEEE IEEE. 2020

    View details for Web of Science ID 000646035600090

  • Verifying Recurrent Neural Networks Using Invariant Inference Jacoby, Y., Barrett, C., Katz, G., Hung, D. V., Sokolsky, O. SPRINGER INTERNATIONAL PUBLISHING AG. 2020: 57-74

    View details for DOI 10.1007/978-3-030-59152-6_3

    View details for Web of Science ID 000723555700003

  • fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components International Conference on Computer Aided Verification Truong, L., Herbst, S., Setaluri, R., Mann, M., Daly, R., Zhang, K., Donovick, C., Stanley, D., Horowitz, M., Barrett, C., Hanrahan, P. 2020

    View details for DOI 10.1007/978-3-030-53288-8_19

  • Creating an Agile Hardware Design Flow Bahr, R., Barrett, C., Bhagdikar, N., Carsello, A., Daly, R., Donovick, C., Durst, D., Fatahalian, K., Feng, K., Hanrahan, P., Hofstee, T., Horowitz, M., Huff, D., Kjolstad, F., Kong, T., Liu, Q., Mann, M., Melchert, J., Nayak, A., Niemetz, A., Nyengele, G., Raina, P., Richardson, S., Setaluri, R., Setter, J., Sreedhar, K., Strange, M., Thomas, J., Torng, C., Truong, L., Tsiskaridze, N., Zhang, K., IEEE IEEE. 2020

    View details for Web of Science ID 000628528400063

  • A-QED Verification of Hardware Accelerators Singh, E., Lonsing, F., Chattopadhyay, S., Strange, M., Wei, P., Zhang, X., Zhou, Y., Chen, D., Cong, J., Raina, P., Zhang, Z., Barrett, C., Mitra, S., IEEE IEEE. 2020

    View details for Web of Science ID 000628528400220

  • Gap-free Processor Verification by S(2)QED and Property Generation Devarajegowda, K., Fadiheh, M., Singh, E., Barrett, C., Mitra, S., Ecker, W., Stoffel, D., Kunz, W., DiNatale, G., Bolchini, C., Vatajelu, E. I. IEEE. 2020: 526–31

    View details for Web of Science ID 000610549200096

  • Selected Extended Papers of NFM 2017: Preface JOURNAL OF AUTOMATED REASONING Barrett, C., Kahsai, T. 2019; 63 (4): 1003–4

    View details for DOI 10.1007/s10817-018-9488-y

    View details for Web of Science ID 000488929300008

  • Refutation-based synthesis in SMT FORMAL METHODS IN SYSTEM DESIGN Reynolds, A., Kuncak, V., Tinelli, C., Barrett, C., Deters, M. 2019; 55 (2): 73–102

    View details for DOI 10.1007/s10703-017-0270-2

    View details for Web of Science ID 000517122100001

  • Reports of the AAAI 2019 Spring Symposium Series AI MAGAZINE Baldini, I., Barrett, C., Chella, A., Cinelli, C., Gamez, D., Gilpin, L. H., Hinkelmann, K., Holmes, D., Kido, T., Kocaoglu, M., Lawless, W. F., Lomuscio, A., Macbeth, J., Martin, A., Mittu, R., Patterson, E., Sofge, D., Tadepalli, P., Takadama, K., Wilson, S. 2019; 40 (3): 59–66

    View details for Web of Science ID 000492858200007

  • G2SAT: Learning to Generate SAT Formulas You, J., Wu, H., Barrett, C., Ramanujan, R., Leskovec, J., Wallach, H., Larochelle, H., Beygelzimer, A., d'Alche-Buc, F., Fox, E., Garnett, R. NEURAL INFORMATION PROCESSING SYSTEMS (NIPS). 2019

    View details for Web of Science ID 000535866902021

  • Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED Lonsing, F., Ganesan, K., Mann, M., Nuthakki, S., Singh, E., Srouji, M., Yang, Y., Mitra, S., Barrett, C., IEEE IEEE. 2019

    View details for Web of Science ID 000524676400055

  • CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis Reynolds, A., Barbosa, H., Notzli, A., Barrett, C., Tinelli, C., Dillig, Tasiran, S. SPRINGER INTERNATIONAL PUBLISHING AG. 2019: 74–83

    View details for DOI 10.1007/978-3-030-25543-5_5

    View details for Web of Science ID 000491468900005

  • High-Level Abstractions for Simplifying Extended String Constraints in SMT Reynolds, A., Notzli, A., Barrett, C., Tinelli, C., Dillig, Tasiran, S. SPRINGER INTERNATIONAL PUBLISHING AG. 2019: 23–42

    View details for DOI 10.1007/978-3-030-25543-5_2

    View details for Web of Science ID 000491468900002

  • The Marabou Framework for Verification and Analysis of Deep Neural Networks Katz, G., Huang, D. A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljic, A., Dill, D. L., Kochenderfer, M. J., Barrett, C., Dillig, Tasiran, S. SPRINGER INTERNATIONAL PUBLISHING AG. 2019: 443–52

    View details for DOI 10.1007/978-3-030-25540-4_26

    View details for Web of Science ID 000491468000026

  • Integration and Flight Test of Small UAS Detect and Avoid on A Miniaturized Avionics Platform Lopez, J. G., Ren, L., Meng, B., Fisher, R., Markham, J., Figard, M., Evans, R., Spoelhof, R., Rubenstahl, M., Edwards, S., Pedan, I., Barrett, C., IEEE IEEE. 2019

    View details for Web of Science ID 000588253200167

  • Invertibility Conditions for Floating-Point Formulas Brain, M., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C., Dillig, Tasiran, S. SPRINGER INTERNATIONAL PUBLISHING AG. 2019: 116–36

    View details for DOI 10.1007/978-3-030-25543-5_8

    View details for Web of Science ID 000491468900008

  • Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking Fadiheh, M., Stoffel, D., Barrett, C., Mitra, S., Kunz, W., IEEE IEEE. 2019: 994–99

    View details for Web of Science ID 000470666100185

  • Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study Singh, E., Devarajegowda, K., Simon, S., Schnieder, R., Ganesan, K., Fadiheh, M., Stoffel, D., Kunz, W., Barrett, C., Ecker, W., Mitra, S., IEEE IEEE. 2019: 1000–1005

    View details for Web of Science ID 000470666100186

  • Verifying Deep-RL-Driven Systems Kazak, Y., Barrett, C., Katz, G., Schapira, M., Assoc Comp Machinery ASSOC COMPUTING MACHINERY. 2019: 83–89

    View details for DOI 10.1145/3341216.3342218

    View details for Web of Science ID 000506862100013

  • G2SAT: Learning to Generate SAT Formulas. Advances in neural information processing systems You, J. n., Wu, H. n., Barrett, C. n., Ramanujan, R. n., Leskovec, J. n. 2019; 32: 10552–63

    Abstract

    The Boolean Satisfiability (SAT) problem is the canonical NP-complete problem and is fundamental to computer science, with a wide array of applications in planning, verification, and theorem proving. Developing and evaluating practical SAT solvers relies on extensive empirical testing on a set of real-world benchmark formulas. However, the availability of such real-world SAT formulas is limited. While these benchmark formulas can be augmented with synthetically generated ones, existing approaches for doing so are heavily hand-crafted and fail to simultaneously capture a wide range of characteristics exhibited by real-world SAT instances. In this work, we present G2SAT, the first deep generative framework that learns to generate SAT formulas from a given set of input formulas. Our key insight is that SAT formulas can be transformed into latent bipartite graph representations which we model using a specialized deep generative neural network. We show that G2SAT can generate SAT formulas that closely resemble given real-world SAT instances, as measured by both graph metrics and SAT solver behavior. Further, we show that our synthetic SAT formulas could be used to improve SAT solver performance on real-world benchmarks, which opens up new opportunities for the continued development of SAT solvers and a deeper understanding of their performance.

    View details for PubMedID 32265581

  • Symbolic Quick Error Detection Using Symbolic Initial State for Pre-Silicon Verification Fadiheh, M., Urdahl, J., Nuthakki, S., Mitra, S., Barrett, C., Stoffel, D., Kunz, W., IEEE IEEE. 2018: 55–60

    View details for Web of Science ID 000435148800010

  • Solving Quantified Bit-Vectors Using Invertibility Conditions Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C., Chockler, H., Weissenbacher, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2018: 236–55

    View details for DOI 10.1007/978-3-319-96142-2_16

    View details for Web of Science ID 000491469700016

  • p4pktgen: Automated Test Case Generation for P4 Programs Notzli, A., Khan, J., Fingerhut, A., Barrett, C., Athanas, P., ACM ASSOC COMPUTING MACHINERY. 2018

    View details for DOI 10.1145/3185467.3185497

    View details for Web of Science ID 000492881200005

  • CoSA: Integrated Verification for Agile Hardware Design Mattarei, C., Mann, M., Barrett, C., Daly, R. G., Huff, D., Hanrahan, P., Bjorner, N., Gurfinkel, A. IEEE. 2018: 7–11

    View details for Web of Science ID 000493916300007

  • REASONING WITH FINITE SETS AND CARDINALITY CONSTRAINTS IN SMT LOGICAL METHODS IN COMPUTER SCIENCE Bansal, K., Barrett, C., Reynolds, A., Tinelli, C. 2018; 14 (4)

    View details for DOI 10.23638/LMCS-14(4:12)2018

    View details for Web of Science ID 000452745300008

  • EMME: A Formal Tool for ECMAScript Memory Model Evaluation Mattarei, C., Barrett, C., Guo, S., Nelson, B., Smith, B., Beyer, D., Huisman, M. SPRINGER INTERNATIONAL PUBLISHING AG. 2018: 55–71

    View details for DOI 10.1007/978-3-319-89963-3_4

    View details for Web of Science ID 000445822600004

  • Datatypes with Shared Selectors Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C., Galmiche, D., Schulz, S., Sebastiani, R. SPRINGER INTERNATIONAL PUBLISHING AG. 2018: 591–608

    View details for DOI 10.1007/978-3-319-94205-6_39

    View details for Web of Science ID 000470004600038

  • Constraint solving for finite model finding in SMT solvers THEORY AND PRACTICE OF LOGIC PROGRAMMING Reynolds, A., Tinelli, C., Barrett, C. 2017; 17 (4): 516–58

    View details for DOI 10.1017/S1471068417000175

    View details for Web of Science ID 000407039000005

  • Towards Proving the Adversarial Robustness of Deep Neural Networks ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE Katz, G., Barrett, C., Dill, D. L., Julian, K., Kochenderfer, M. J. 2017: 19–26

    View details for DOI 10.4204/EPTCS.257.3

    View details for Web of Science ID 000439354100004

  • Designing Theory Solvers with Extensions Reynolds, A., Tinelli, C., Jovanovic, D., Barrett, C., Dixon, C., Finger, M. SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 22–40

    View details for DOI 10.1007/978-3-319-66167-4_2

    View details for Web of Science ID 000439925700002

  • Partitioned Memory Models for Program Analysis Wang, W., Barrett, C., Wies, T., Bouajjani, A., Monniaux, D. SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 539–58

    View details for DOI 10.1007/978-3-319-52234-0_29

    View details for Web of Science ID 000413069800029

  • E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods Singh, E., Barrett, C., Mitra, S., Majumdar, R., Kuncak SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 104–25

    View details for DOI 10.1007/978-3-319-63390-9_6

    View details for Web of Science ID 000431900900006

  • Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks Katz, G., Barrett, C., Dill, D. L., Julian, K., Kochenderfer, M. J., Majumdar, R., Kuncak SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 97–117

    View details for DOI 10.1007/978-3-319-63387-9_5

    View details for Web of Science ID 000432196400005

  • Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C., Majumdar, R., Kuncak SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 453–74

    View details for DOI 10.1007/978-3-319-63390-9_24

    View details for Web of Science ID 000431900900024

  • Relational Constraint Solving in SMT Meng, B., Reynolds, A., Tinelli, C., Barrett, C., DeMoura, L. SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 148–65

    View details for DOI 10.1007/978-3-319-63046-5_10

    View details for Web of Science ID 000437512300010

  • Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions IEEE DESIGN & TEST Singh, E., Lin, D., Barrett, C., Mitra, S. 2016; 33 (6): 55-62

    View details for DOI 10.1109/MDAT.2016.2590987

    View details for Web of Science ID 000393047000009

  • An efficient SMT solver for string constraints FORMAL METHODS IN SYSTEM DESIGN Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., Deters, M. 2016; 48 (3): 206–34

    View details for DOI 10.1007/s10703-016-0247-6

    View details for Web of Science ID 000382702200003

  • Lazy Proofs for DPLL(T)-Based SMT Solvers Katz, G., Barrett, C., Tinelli, C., Reynolds, A., Hadarean, L., Piskac, R., Talupur, M. IEEE. 2016: 93–100

    View details for Web of Science ID 000406120700020

  • Efficient solving of string constraints for security analysis Barrett, C., Tinelli, C., Deters, M., Liang, T., Reynolds, A., Tsiskaridze, N., ACM ASSOC COMPUTING MACHINERY. 2016: 4–6

    View details for DOI 10.1145/2898375.2898393

    View details for Web of Science ID 000392435600004

  • Structured Approach to Post-Silicon Validation and Debug Using Symbolic Quick Error Detection Lin, D., Singh, E., Barrett, C., Mitra, S., IEEE IEEE. 2015

    View details for Web of Science ID 000370747500019

  • A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C., Lutz, C., Ranise, S. SPRINGER-VERLAG BERLIN. 2015: 135–50

    View details for DOI 10.1007/978-3-319-24246-0_9

    View details for Web of Science ID 000366183700009

  • Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors Hadarean, L., Barrett, C., Reynolds, A., Tinelli, C., Deters, M., Davis, M., Fehnker, A., McIver, A., Voronkov, A. SPRINGER INT PUBLISHING AG. 2015: 340–55

    View details for DOI 10.1007/978-3-662-48899-7_24

    View details for Web of Science ID 000375574900024

  • Cascade 2.0 Wang, W., Barrett, C., Wies, T., McMillan, K. L., Rival SPRINGER-VERLAG BERLIN. 2014: 142–60

    View details for Web of Science ID 000354781700009

  • 6 Years of SMT-COMP JOURNAL OF AUTOMATED REASONING Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A. 2013; 50 (3): 243–77

    View details for DOI 10.1007/s10817-012-9246-5

    View details for Web of Science ID 000314314800001

  • Being careful about theory combination FORMAL METHODS IN SYSTEM DESIGN Jovanovic, D., Barrett, C. 2013; 42 (1): 67-90

    View details for DOI 10.1007/s10703-012-0159-z

    View details for Web of Science ID 000313365300005

  • The Design and Implementation of the Model Constructing Satisfiability Calculus Jovanovic, D., Barrett, C., de Moura, L., IEEE IEEE. 2013: 173–80

    View details for Web of Science ID 000333262700025

  • Witness Runs for Counter Machines Barrett, C., Demri, S., Deters, M., Galmiche, D., LarcheyWendling, D. SPRINGER-VERLAG BERLIN. 2013: 1–4

    View details for Web of Science ID 000345041900001

  • Witness Runs for Counter Machines Barrett, C., Demri, S., Deters, M., Fontaine, P., Ringeissen, C., Schmidt, R. A. SPRINGER-VERLAG BERLIN. 2013: 120–50

    View details for Web of Science ID 000329707100009

  • Simplex with Sum of Infeasibilities for SMT King, T., Barrett, C., Dutertre, B., IEEE IEEE. 2013: 189–96

    View details for Web of Science ID 000333262700027

  • The SMT-LIB Initiative and the Rise of SMT (HVC 2010 Award Talk) Barrett, C., de Moura, L., Ranise, S., Stump, A., Tinelli, C., Barner, S., Harris, Kroening, D., Raz, O. SPRINGER-VERLAG BERLIN. 2011: 3

    View details for Web of Science ID 000296687000002

  • Sharing Is Caring: Combination of Theories Jovanovic, D., Barrett, C., Tinelli, C., SofronieStokkermans SPRINGER-VERLAG BERLIN. 2011: 195–210

    View details for Web of Science ID 000307792600014

  • Polite Theories Revisited Jovanovic, D., Barrett, C., Fermuller, C. G., Voronkov, A. SPRINGER-VERLAG BERLIN. 2010: 402–16

    View details for DOI 10.1007/978-3-642-16242-8_29

    View details for Web of Science ID 000288062700029

  • Verifying Low-Level Implementations of High-Level Datatypes Conway, C. L., Barrett, C., Touili, T., Cook, B., Jackson, P. SPRINGER-VERLAG BERLIN. 2010: 306–20

    View details for Web of Science ID 000281446200027

  • Solving quantified verification conditions using satisfiability modulo theories ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE Ge, Y., Barrett, C., Tinelli, C. 2009; 55 (1-2): 101–22

    View details for DOI 10.1007/s10472-009-9153-6

    View details for Web of Science ID 000270579000005

  • Satisfiability Modulo Theories HANDBOOK OF SATISFIABILITY Barrett, C., Sebastiani, R., Seshia, S. A., Tinelli, C., Biere, A., Heule, M., VanMaaren, H., Walsh, T. 2009; 185: 825–85

    View details for DOI 10.3233/978-1-58603-929-5-825

    View details for Web of Science ID 000271674900026

  • DESIGN AND RESULTS OF THE 3RD ANNUAL SATISFIABILITY MODULO THEORIES COMPETITION (SMT-COMP 2007) INTERNATIONAL JOURNAL ON ARTIFICIAL INTELLIGENCE TOOLS Barrett, C., Deters, M., Oliveras, A., Stump, A. 2008; 17 (4): 569-606

    View details for Web of Science ID 000260806800001

  • Pointer analysis, conditional soundness, and proving the absence of errors STATIC ANALYSIS Conway, C. L., Dams, D., Namjoshi, K. S., Barrett, C. 2008; 5079: 62-77

    View details for Web of Science ID 000257884600005

  • Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) FORMAL METHODS IN SYSTEM DESIGN Barrett, C., de Moura, L., Stump, A. 2007; 31 (3): 221-239

    View details for DOI 10.1007/s10703-007-0038-1

    View details for Web of Science ID 000250580800002

  • CVC3 - (Tool paper) COMPUTER AIDED VERIFICATION, PROCEEDINGS Barrett, C., Tinelli, C. 2007; 4590: 298-302

    View details for Web of Science ID 000248222700031

  • Cascade: C assertion checker and deductive engine (Tool paper) COMPUTER AIDED VERIFICATION, PROCEEDINGS Sethi, N., Barrett, C. 2006; 4144: 166-169

    View details for Web of Science ID 000240257000015

  • Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) JOURNAL OF AUTOMATED REASONING Barrett, C., de Moura, L., Stump, A. 2005; 35 (4): 373-390

    View details for DOI 10.1007/s10817-006-9026-1

    View details for Web of Science ID 000241379200003

  • TVOC: A translation validator for optimizing compilers COMPUTER AIDED VERIFICATION, PROCEEDINGS Barrett, C., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L. 2005; 3576: 291-295

    View details for Web of Science ID 000230755800029

  • CVC Lite: A new implementation of the cooperating validity checker COMPUTER AIDED VERIFICATION Barrett, C., Berezin, S. 2004; 3114: 515-518

    View details for Web of Science ID 000222865000049

  • A generalization of Shostak's method for combining decision procedures 4th International Workshop on Frontiers of Combining Systems Barrett, C. W., Dill, D. L., Stump, A. SPRINGER-VERLAG BERLIN. 2002: 132–146

    View details for Web of Science ID 000181051800011

  • A framework for cooperating decision procedures 17th International Conference on Automated Deduction (CADE-17) Barrett, C. W., Dill, D. L., Stump, A. SPRINGER-VERLAG BERLIN. 2000: 79–98

    View details for Web of Science ID 000166717300006

  • A decision procedure for bit-vector arithmetic 35th Design Automation Conference Barrett, C. W., Dill, D. L., LEVITT, J. R. ASSOC COMPUTING MACHINERY. 1998: 522–527

    View details for Web of Science ID 000077273700094

  • Validity checking for combinations of theories with equality 1st International Conference on Formal Methods in Computer-Aided Design (FMCAD 96) Barrett, C., Dill, D., LEVITT, J. SPRINGER-VERLAG BERLIN. 1996: 187–201

    View details for Web of Science ID 000073935500013

https://orcid.org/0000-0002-9522-3084