Clark Barrett
Professor (Research) of Computer Science
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 2021 Computer Aided Verification (CAV) award.
Administrative Appointments
-
Director, Center for Automated Reasoning (Centaur) (2021 - Present)
-
Co-director, Center for AI Safety (2019 - Present)
-
Visiting Scientist, Google (2015 - 2017)
Honors & Awards
-
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
-
Independent Studies (12)
- Advanced Reading and Research
CS 499 (Aut, Win, Spr) - Advanced Reading and Research
CS 499P (Aut, Win, Spr) - Curricular Practical Training
CS 390A (Aut, Win, Spr) - Curricular Practical Training
CS 390B (Aut, Win, Spr) - Curricular Practical Training
CS 390C (Aut, Win, Spr) - Independent Project
CS 399 (Aut, Win, Spr) - Independent Work
CS 199 (Aut, Win, Spr) - Independent Work
CS 199P (Aut, Win, Spr) - Part-time Curricular Practical Training
CS 390D (Aut, Win, Spr) - Senior Honors Thesis
MATH 197 (Win, Spr) - Supervised Undergraduate Research
CS 195 (Aut, Win, Spr) - Writing Intensive Senior Research Project
CS 191W (Aut, Win, Spr)
- Advanced Reading and Research
Stanford Advisees
-
Doctoral Dissertation Reader (AC)
Nikhil Bhagdikar, Yao Hsiao, Gabriel Poesia Reis e Silva, Eshan Singh, Lenny Truong -
Postdoctoral Faculty Sponsor
Pei Huang, Min Wu -
Doctoral Dissertation Advisor (AC)
Samuel Akinwande -
Orals Evaluator
Lenny Truong -
Master's Program Advisor
Anushree Aggarwal, Artem Arzyn, Kiran Bhat, Lavender Chen, Alina Hu, Nick Mecklenburg, Aakash Mishra, Narvin Phouksouvath, Kaiyu Ren, Cole Sprout, Sudharsan Sundar, Justin Wei, Sam Wondsen -
Doctoral Dissertation Co-Advisor (AC)
Robert Moss, Alex Ozdemir -
Doctoral (Program)
Daneshvar Amrollahi, Leni Aniva, Rachel Cleaveland, Hanna Lachnitt, Abdal Mohamed, Áron Ricardo Perez-Lopez, Liza Pertseva, Livia Sun, Scott Viteri, Amalee Wilson
All Publications
-
IsaRARE: Automatic Verification of SMT Rewrites in Isabelle/HOL
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
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
-
Combining Stable Infiniteness and (Strong) Politeness
JOURNAL OF AUTOMATED REASONING
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
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
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
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
-
VERIX: Towards Verified Explainability of Deep Neural Networks
NEURAL INFORMATION PROCESSING SYSTEMS (NIPS). 2023
View details for Web of Science ID 001230083404006
-
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators
IEEE. 2023
View details for DOI 10.1109/DAC56929.2023.10247903
View details for Web of Science ID 001073487300211
-
Toward Certified Robustness Against Real-World Distribution Shifts
IEEE COMPUTER SOC. 2023: 537-553
View details for DOI 10.1109/SaTML54575.2023.00042
View details for Web of Science ID 001012311500032
-
On Optimal Caching and Model Multiplexing for Large Model Inference
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
NEURAL INFORMATION PROCESSING SYSTEMS (NIPS). 2023
View details for Web of Science ID 001224281503036
-
AHA: An Agile Approach to the Design of Coarse-Grained Reconfigurable Accelerators and Compilers
ACM Transactions on Embedded Computing Systems
2023; 22 (2)
View details for DOI 10.1145/3534933
-
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness
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
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
-
Formal Verification of Bit-Vector Invertibility Conditions in Coq
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
-
<i>Soy</i>: An Efficient MILP Solver for Piecewise-Affine Systems
IEEE. 2023: 6281-6288
View details for DOI 10.1109/IROS55552.2023.10342011
View details for Web of Science ID 001136907800122
-
Scalable Verification of GNN-Based Job Schedulers
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
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
2022
View details for DOI 10.1007/s10817-022-09625-3
View details for Web of Science ID 000791156700001
-
Neural Network Verification with Proof Production
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
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
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
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
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
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)
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
-
Flexible Proof Production in an Industrial-Strength SMT Solver
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
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
-
Efficient Neural Network Analysis with Sum-of-Infeasibilities
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
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
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
-
Even Faster Conflicts and Lazier Reductions for String Solvers
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
-
Global optimization of objective functions represented by ReLU networks
MACHINE LEARNING
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
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
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
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
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
-
Smt-Switch: A Solver-Agnostic C plus plus API for SMT Solving
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
-
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers
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
2021; 18 (3)
View details for DOI 10.46298/LMCS-18(3:26)2022
View details for Web of Science ID 000860394200002
-
Politeness and Stable Infiniteness: Stronger Together
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
-
Creating an Agile Hardware Design Flow
IEEE. 2020
View details for Web of Science ID 000628528400063
-
Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance
IEEE. 2020
View details for Web of Science ID 000646035600090
-
Gap-free Processor Verification by S(2)QED and Property Generation
IEEE. 2020: 526–31
View details for Web of Science ID 000610549200096
-
Verifying Recurrent Neural Networks Using Invariant Inference
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
-
The Move Prover
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
-
A-QED Verification of Hardware Accelerators
IEEE. 2020
View details for Web of Science ID 000628528400220
-
fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components
International Conference on Computer Aided Verification
2020
View details for DOI 10.1007/978-3-030-53288-8_19
-
Selected Extended Papers of NFM 2017: Preface
JOURNAL OF AUTOMATED REASONING
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
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
2019; 40 (3): 59–66
View details for Web of Science ID 000492858200007
-
Verifying Deep-RL-Driven Systems
ASSOC COMPUTING MACHINERY. 2019: 83–89
View details for DOI 10.1145/3341216.3342218
View details for Web of Science ID 000506862100013
-
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED
IEEE. 2019
View details for Web of Science ID 000524676400055
-
G2SAT: Learning to Generate SAT Formulas
NEURAL INFORMATION PROCESSING SYSTEMS (NIPS). 2019
View details for Web of Science ID 000535866902021
-
Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking
IEEE. 2019: 994–99
View details for Web of Science ID 000470666100185
-
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study
IEEE. 2019: 1000–1005
View details for Web of Science ID 000470666100186
-
G2SAT: Learning to Generate SAT Formulas.
Advances in neural information processing systems
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
-
CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
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
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
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
IEEE. 2019
View details for Web of Science ID 000588253200167
-
Invertibility Conditions for Floating-Point Formulas
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
-
Symbolic Quick Error Detection Using Symbolic Initial State for Pre-Silicon Verification
IEEE. 2018: 55–60
View details for Web of Science ID 000435148800010
-
Datatypes with Shared Selectors
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
-
Solving Quantified Bit-Vectors Using Invertibility Conditions
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
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
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
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
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
-
Constraint solving for finite model finding in SMT solvers
THEORY AND PRACTICE OF LOGIC PROGRAMMING
2017; 17 (4): 516–58
View details for DOI 10.1017/S1471068417000175
View details for Web of Science ID 000407039000005
-
Relational Constraint Solving in SMT
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
-
Designing Theory Solvers with Extensions
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
-
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification
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
-
Partitioned Memory Models for Program Analysis
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
-
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
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
-
Towards Proving the Adversarial Robustness of Deep Neural Networks
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
2017: 19–26
View details for DOI 10.4204/EPTCS.257.3
View details for Web of Science ID 000439354100004
-
E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods
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
-
Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions
IEEE DESIGN & TEST
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
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
IEEE. 2016: 93–100
View details for Web of Science ID 000406120700020
-
Efficient solving of string constraints for security analysis
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
IEEE. 2015
View details for Web of Science ID 000370747500019
-
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
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
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
SPRINGER-VERLAG BERLIN. 2014: 142–60
View details for Web of Science ID 000354781700009
-
6 Years of SMT-COMP
JOURNAL OF AUTOMATED REASONING
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
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
IEEE. 2013: 173–80
View details for Web of Science ID 000333262700025
-
Witness Runs for Counter Machines
SPRINGER-VERLAG BERLIN. 2013: 1–4
View details for Web of Science ID 000345041900001
-
Witness Runs for Counter Machines
SPRINGER-VERLAG BERLIN. 2013: 120–50
View details for Web of Science ID 000329707100009
-
Simplex with Sum of Infeasibilities for SMT
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)
SPRINGER-VERLAG BERLIN. 2011: 3
View details for Web of Science ID 000296687000002
-
Sharing Is Caring: Combination of Theories
SPRINGER-VERLAG BERLIN. 2011: 195–210
View details for Web of Science ID 000307792600014
-
Polite Theories Revisited
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
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
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
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
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
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
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
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
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
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
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
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
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)
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
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)
SPRINGER-VERLAG BERLIN. 1996: 187–201
View details for Web of Science ID 000073935500013