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

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


  • The Nonexistence of Unicorns and Many-Sorted Lowenheim-Skolem Theorems Przybocki, B., Toledo, G., Zohar, Y., Barrett, C., Platzer, A., Rozier, K. Y., Pradella, M., Rossi, M. SPRINGER INTERNATIONAL PUBLISHING AG. 2025: 658-675
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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)
  • 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)
  • 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

  • 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

  • Satisfiability Modulo Finite Fields Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C., Enea, C., Lal, A. SPRINGER INTERNATIONAL PUBLISHING AG. 2023: 163-186
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • <i>Soy</i>: An Efficient MILP Solver for Piecewise-Affine Systems Wu, H., Wu, M., Sadigh, D., Barrett, C., IEEE IEEE. 2023: 6281-6288
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • <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
  • 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
  • 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
  • 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
  • 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
  • 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
  • Towards Satisfiability Modulo Parametric Bit-vectors JOURNAL OF AUTOMATED REASONING Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C. 2021
  • 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
  • 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
  • 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)
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • Selected Extended Papers of NFM 2017: Preface JOURNAL OF AUTOMATED REASONING Barrett, C., Kahsai, T. 2019; 63 (4): 1003–4
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • Verifying Deep-RL-Driven Systems Kazak, Y., Barrett, C., Katz, G., Schapira, M., Assoc Comp Machinery ASSOC COMPUTING MACHINERY. 2019: 83–89
  • 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

  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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)
  • 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
  • p4pktgen: Automated Test Case Generation for P4 Programs Notzli, A., Khan, J., Fingerhut, A., Barrett, C., Athanas, P., ACM ASSOC COMPUTING MACHINERY. 2018
  • 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
  • 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
  • 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
  • Partitioned Memory Models for Program Analysis Wang, W., Barrett, C., Wies, T., Bouajjani, A., Monniaux, D. SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 539–58
  • 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
  • Relational Constraint Solving in SMT Meng, B., Reynolds, A., Tinelli, C., Barrett, C., DeMoura, L. SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 148–65
  • Designing Theory Solvers with Extensions Reynolds, A., Tinelli, C., Jovanovic, D., Barrett, C., Dixon, C., Finger, M. SPRINGER INTERNATIONAL PUBLISHING AG. 2017: 22–40
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • Cascade 2.0 Wang, W., Barrett, C., Wies, T., McMillan, K. L., Rival SPRINGER-VERLAG BERLIN. 2014: 142–60
  • 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
  • Being careful about theory combination FORMAL METHODS IN SYSTEM DESIGN Jovanovic, D., Barrett, C. 2013; 42 (1): 67-90
  • The Design and Implementation of the Model Constructing Satisfiability Calculus Jovanovic, D., Barrett, C., de Moura, L., IEEE IEEE. 2013: 173–80
  • Witness Runs for Counter Machines Barrett, C., Demri, S., Deters, M., Galmiche, D., LarcheyWendling, D. SPRINGER-VERLAG BERLIN. 2013: 1–4
  • Witness Runs for Counter Machines Barrett, C., Demri, S., Deters, M., Fontaine, P., Ringeissen, C., Schmidt, R. A. SPRINGER-VERLAG BERLIN. 2013: 120–50
  • Simplex with Sum of Infeasibilities for SMT King, T., Barrett, C., Dutertre, B., IEEE IEEE. 2013: 189–96
  • 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
  • Sharing Is Caring: Combination of Theories Jovanovic, D., Barrett, C., Tinelli, C., SofronieStokkermans SPRINGER-VERLAG BERLIN. 2011: 195–210
  • Polite Theories Revisited Jovanovic, D., Barrett, C., Fermuller, C. G., Voronkov, A. SPRINGER-VERLAG BERLIN. 2010: 402–16
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • CVC3 - (Tool paper) COMPUTER AIDED VERIFICATION, PROCEEDINGS Barrett, C., Tinelli, C. 2007; 4590: 298-302
  • Cascade: C assertion checker and deductive engine (Tool paper) COMPUTER AIDED VERIFICATION, PROCEEDINGS Sethi, N., Barrett, C. 2006; 4144: 166-169
  • 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
  • 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
  • CVC Lite: A new implementation of the cooperating validity checker COMPUTER AIDED VERIFICATION Barrett, C., Berezin, S. 2004; 3114: 515-518
  • 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
  • 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
  • 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
  • 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