Clark Barrett

Stanford Medicine — United States

Computer Science · Physical Sciences

42h-index10.2kcitations291works2.62yr avg
OpenAlex↗ORCID↗Google Scholar↗Lab page↗

Accepting Students?

No reports yet. Know if this professor is taking students?

Research Topics

Formal Methods in Verification(141), Logic, programming, and type systems(104), Software Testing and Debugging Techniques(52), Adversarial Robustness in Machine Learning(46), Logic, Reasoning, and Knowledge(32)

Publications291 total

Combining Combination Properties, Part I: Nelson-Oppen and Politeness
Journal of Automated Reasoning·2025Open Access
Certificates in AI: Learn but Verify
Communications of the ACM·2025Open Access
Proof Minimization in Neural Network Verification
arXiv (Cornell University)·2025Open Access
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
arXiv (Cornell University)·2025Open Access
ClassInvGen: Class Invariant Synthesis Using Large Language Models
Lecture notes in computer science·2025· 1 cited
Interactive Bitvector Reasoning using Verified Bit-Blasting
Proceedings of the ACM on Programming Languages·2025Open Access
Solving Set Constraints with Comprehensions and Bounded Quantifiers
arXiv (Cornell University)·2025Open Access
Integer Reasoning Modulo Different Constants in SMT
arXiv (Cornell University)·2025Open Access
Lean-SMT: An SMT tactic for discharging proof goals in Lean
arXiv (Cornell University)·2025Open Access
Relational Hoare Logic for Realistically Modelled Machine Code
arXiv (Cornell University)·2025Open Access
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
arXiv (Cornell University)·2025· 1 citedOpen Access
Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs
Formal Methods in System Design·2025
Cubing for Tuning
arXiv (Cornell University)·2025Open Access
Efficient SAT-Based Bounded Model Checking of Evolving Systems
2025
Application of Formal Methods (SAT/SMT) to the Design of Constrained Codes
2025
Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures
arXiv (Cornell University)·2025Open Access
ClassInvGen: Class Invariant Synthesis using Large Language Models
arXiv (Cornell University)·2025Open Access
The termination of Nielsen transformations applied to word equations with length constraints
arXiv (Cornell University)·2025· 1 citedOpen Access
Integer Reasoning Modulo Different Constants in SMT
Lecture notes in computer science·2025Open Access
Relational Hoare Logic for Realistically Modelled Machine Code
Lecture notes in computer science·2025· 1 citedOpen Access
page 1 of 15Next →

Frequent Co-authors

Cesare Tinelli(18), David L. Dill(12), Andrew Reynolds(10), Aaron Stump(8), Guy Katz(7), Morgan Deters(7), Mykel J. Kochenderfer(6), Kyle D. Julian(4), Dejan Jovanović(4), Guy Katz(4), Christopher Lazarus(3), Haniel Barbosa(3), Andres Nötzli(3), Jeremy Levitt(3), Tianyi Liang(3), Albert Oliveras(3), Nicholas Carlini(3), Leonardo de Moura(3), Benjamin Goldberg(3), Lenore D. Zuck(3)