Bio


Clark Barrett joined Stanford University as an Associate Professor (Research) of Computer Science in September 2016. Before that, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. His expertise is in constraint solving and its applications to system verification and security. His PhD dissertation introduced a novel approach to constraint solving now known as Satisfiability Modulo Theories (SMT). Today, he is recognized as one of the world's experts in the development and application of SMT techniques. He was also an early pioneer in the development of formal hardware verification: at Intel, he collaborated on a novel theorem prover used to verify key microprocessor properties; and at 0-in Design Automation (now part of Mentor Graphics), he helped build one of the first industrially successful assertion-based verification tool-sets for hardware. He is an ACM Distinguished Scientist.

Academic Appointments


Administrative Appointments


  • Visiting Scientist, Google (2015 - Present)

Honors & Awards


  • Distinguished Scientist, ACM (2014)
  • HVC Award, Haifa Verification Conference (2010)
  • Software Quality Innovation Award, IBM (2008)
  • CAREER award, National Science Foundation (2007)
  • Best Paper, Design Automation Conference (1998)

Professional Education


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

Patents


  • Jeremy R. Levitt, Christophe G. Gauthron, Clark W. Barrett, Lawrence Curtis Widdoes Jr. "United States Patent 20070299648 Reuse of learned information to simplify functional verification of a digital circuit", Dec 27, 2007

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 and software 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.

The starting point for this vision is a new class of logical engines based on Satisfiability Modulo Theories (SMT)}, an emerging research area I helped found as part of my PhD dissertation in 2003. My research agenda focuses on advancing the theory, implementation, and applications of SMT. The primary vehicle for this research is an open-source SMT solver called CVC4 (see cvc4.cs.stanford.edu). Some current applications of SMT that my group is working on include automatically finding bugs in hardware and software, automatically finding security vulnerabilities, and automatically verifying the safety of autonomous controllers generated using machine learning.

Projects


  • CVC4 (9/1/2009 - Present)

    An open-source SMT solver

    Location

    Stanford, CA

    Collaborators

    • Cesare Tinelli, Professor, University of Iowa

    For More Information:

Stanford Advisees


All Publications


  • 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
  • Being careful about theory combination FORMAL METHODS IN SYSTEM DESIGN Jovanovic, D., Barrett, C. 2013; 42 (1): 67-90
  • 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