Publications (101)
Verifying SQL Queries using Theories of Tables and Relations
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli +1
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
Leni Aniva, Chuyue Sun, Brando Miranda +2
Safe and Reliable Training of Learning-Based Aerospace Controllers
Udayan Mandal, Guy Amir, Haoze Wu +10
Global Optimization of Objective Functions Represented by ReLU Networks
Christopher A. Strong, Haoze Wu, Aleksandar ZeljiÄ +4
Toward Scalable Verification for Safety-Critical Deep Networks
Lindsey Kuper, Guy Katz, Justin Gottschlich +3
Towards Bit-Width-Independent Proofs in SMT Solvers
Aina Niemetz, Mathias Preiner, Andrew Reynolds +3
Towards Efficient Verification of Quantized Neural Networks
Pei Huang, Haoze Wu, Yuting Yang +4
Convex Bounds on the Softmax Function with Applications to Robustness Verification
Dennis Wei, Haoze Wu, Min Wu +3
The termination of Nielsen transformations applied to word equations with length constraints
Benjamin Przybocki, Clark Barrett
Identifying and Mitigating the Security Risks of Generative AI
Clark Barrett, Brad Boyd, Elie Burzstein +20
lazybvtoint at the SMT Competition 2020
Yoni Zohar, Ahmed Irfan, Makai Mann +3
An AI Approach to Verified Production Cryptographic Libraries
Chuyue Sun, Su Fong, Zhiyi Kuang +5
HO: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models
Zhenyu Zhang, Ying Sheng, Tianyi Zhou +9
Faithful Autoformalization via Roundtrip Verification and Repair
Daneshvar Amrollahi, Jerry Lopez, Clark Barrett
CVC4 at the SMT Competition 2018
Clark Barrett, Haniel Barbosa, Martin Brain +8
On Optimizing Back-Substitution Methods for Neural Network Verification
Tom Zelazny, Haoze Wu, Clark Barrett +1
CSLib: The Lean Computer Science Library
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi +5
Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers
Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu +2
Relational Hoare Logic for Realistically Modelled Machine Code
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee +4
Simplifying Neural Networks using Formal Verification
Sumathi Gokulanathan, Alexander Feldsher, Adi Malca +2
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Haoze Wu, Omri Isac, Aleksandar ZeljiÄ +14
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Udayan Mandal, Guy Amir, Haoze Wu +9
Generalized Optimization Modulo Theories
Nestan Tsiskaridze, Clark Barrett, Cesare Tinelli
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study
Eshan Singh, Keerthikumara Devarajegowda, Sebastian Simon +8
Lookahead Branching for Neural Network Verification
Liam Davis, Duo Zhou, Huan Zhang +3
Politeness for the Theory of Algebraic Datatypes
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
CVC4SY for SyGuS-COMP 2019
Andrew Reynolds, Haniel Barbosa, Andres Nötzli +2
PEak: A Single Source of Truth for Hardware Design and Verification
Caleb Donovick, Ross Daly, Jackson Melchert +4
Toward Certified Robustness Against Real-World Distribution Shifts
Haoze Wu, Teruhiro Tagomori, Alexander Robey +6
Towards SMT Solver Stability via Input Normalization
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz +4
On Optimal Caching and Model Multiplexing for Large Model Inference
Banghua Zhu, Ying Sheng, Lianmin Zheng +3
Automated Reasoning with Nested Datatypes
Tomer Hakak, Yoni Zohar, Andrew Reynolds +2
Polyhedral Enclosures: An Efficient Combinatorial Abstraction for Nonlinear Neural Feedback Systems
I. Samuel Akinwande, Chelsea Sidrane, Mykel J. Kochenderfer +1
EMME: a formal tool for ECMAScript Memory Model Evaluation
Cristian Mattarei, Clark Barrett, Shu-yu Guo +3
A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems
Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer +1
Solving Set Constraints with Comprehensions and Bounded Quantifiers
Mudathir Mohamed, Nick Feng, Andrew Reynolds +3
Towards Proving the Adversarial Robustness of Deep Neural Networks
Guy Katz, Clark Barrett, David L. Dill +2
Smt-Switch: a solver-agnostic C++ API for SMT Solving
Makai Mann, Amalee Wilson, Cesare Tinelli +1
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
David "davidad" Dalrymple, Joar Skalse, Yoshua Bengio +14
FlexGen: High-Throughput Generative Inference of Large Language Models with a Single GPU
Ying Sheng, Lianmin Zheng, Binhang Yuan +11
An SMT-Based Approach for Verifying Binarized Neural Networks
Guy Amir, Haoze Wu, Clark Barrett +1
Reasoning About Vectors using an SMT Theory of Sequences
Ying Sheng, Andres Nötzli, Andrew Reynolds +7
DNN Verification, Reachability, and the Exponential Function Problem
Omri Isac, Yoni Zohar, Clark Barrett +1
DRAT-based Bit-Vector Proofs in CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner +2
VeriX: Towards Verified Explainability of Deep Neural Networks
Min Wu, Haoze Wu, Clark Barrett
Clover: Closed-Loop Verifiable Code Generation
Chuyue Sun, Ying Sheng, Oded Padon +1
G2SAT: Learning to Generate SAT Formulas
Jiaxuan You, Haoze Wu, Clark Barrett +2
Automated Design Space Exploration of CGRA Processing Element Architectures using Frequent Subgraph Analysis
Jackson Melchert, Kathleen Feng, Caleb Donovick +5
On Deciding Local Theory Extensions via E-matching
Kshitij Bansal, Andrew Reynolds, Tim King +2
Automating Bitvector and Finite Field Equivalence Proofs in Lean
Elizaveta Pertseva, Valentin Robert, Clark Barrett +1
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection
Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki +6
fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
Lenny Truong, Steven Herbst, Rajsekhar Setaluri +8
Partitioning Strategies for Distributed SMT Solving
Amalee Wilson, Andres Noetzli, Andrew Reynolds +3
The FABRIC Strategy for Verifying Neural Feedback Systems
Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer +1
The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
Benjamin Przybocki, Guilherme Toledo, Yoni Zohar +1
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni +12
Automating System Configuration
Nestan Tsiskaridze, Maxwell Strange, Makai Mann +4
Self-Supervised Bootstrapping of Action-Predictive Embodied Reasoning
Milan Ganai, Katie Luo, Jonas Frey +2
Verifying Recurrent Neural Networks using Invariant Inference
Yuval Jacoby, Clark Barrett, Guy Katz
ClassInvGen: Class Invariant Synthesis using Large Language Models
Chuyue Sun, Viraj Agashe, Saikat Chakraborty +5
Reasoning with Finite Sets and Cardinality Constraints in SMT
Kshitij Bansal, Clark Barrett, Andrew Reynolds +1
Efficiently Computing Compact Formal Explanations
Min Wu, Xiaofu Li, Haoze Wu +1
Neural Network Verification with Proof Production
Omri Isac, Clark Barrett, Min Zhang +1
Algorithms for Verifying Deep Neural Networks
Changliu Liu, Tomer Arnon, Christopher Lazarus +3
Integer Reasoning Modulo Different Constants in SMT
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor +4
Parallelization Techniques for Verifying Neural Networks
Haoze Wu, Alex Ozdemir, Aleksandar ZeljiÄ +7
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness
Guilherme Vicentin de Toledo, Yoni Zohar, Clark Barrett
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar +2
Provably Minimally-Distorted Adversarial Examples
Nicholas Carlini, Guy Katz, Clark Barrett +1
Lean-SMT: An SMT tactic for discharging proof goals in Lean
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan +5
Proof Minimization in Neural Network Verification
Omri Isac, Idan Refaeli, Haoze Wu +2
Soy: An Efficient MILP Solver for Piecewise-Affine Systems
Haoze Wu, Min Wu, Dorsa Sadigh +1
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Makai Mann, Ahmed Irfan, Alberto Griggio +2
DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks
Divya Gopinath, Guy Katz, Corina S. Pasareanu +1
Tighter Abstract Queries in Neural Network Verification
Elazar Cohen, Yizhak Yisrael Elboher, Clark Barrett +1
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Haoze Wu, Christopher Hahn, Florian Lonsing +3
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
Yicheng Qian, Joshua Clune, Clark Barrett +1
Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking
Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark Barrett +2
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4
Andrew Reynolds, Morgan Deters, Viktor Kuncak +2
Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4
Leni Aniva, Iori Oikawa, David Dill +1
On Solving Quantified Bit-Vectors using Invertibility Conditions
Aina Niemetz, Mathias Preiner, Andrew Reynolds +2
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Guy Katz, Clark Barrett, David Dill +2
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi +5
PICID: Proof-Driven Clause Learning in Neural Network Verification
Omri Isac, Idan Refaeli, Haoze Wu +2
Politeness and Stable Infiniteness: Stronger Together
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
A Theoretical Framework for Symbolic Quick Error Detection
Florian Lonsing, Subhasish Mitra, Clark Barrett
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection
Ross Daly, Caleb Donovick, Caleb Terrill +4
E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal Methods
Eshan Singh, Clark Barrett, Subhasish Mitra
Combining Finite Combination Properties: Finite Models and Busy Beavers
Guilherme Toledo, Yoni Zohar, Clark Barrett
Logic Bug Detection and Localization Using Symbolic Quick Error Detection
Eshan Singh, David Lin, Clark Barrett +1
Efficient Neural Network Analysis with Sum-of-Infeasibilities
Haoze Wu, Aleksandar ZeljiÄ, Guy Katz +1
Constraint Solving for Finite Model Finding in SMT Solvers
Andrew Reynolds, Cesare Tinelli, Clark Barrett
DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers
Colin Paterson, Haoze Wu, John Grese +3
SGLang: Efficient Execution of Structured Language Model Programs
Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie +9
Lemur: Integrating Large Language Models in Automated Program Verification
Haoze Wu, Clark Barrett, Nina Narodytska
Satisfiability Modulo Extensional Constant Arrays (Extended Version)
Mathias Preiner, Aina Niemetz, Clark Barrett
Markovian Transformers for Informative Language Modeling
Scott Viteri, Max Lamparth, Peter Chatain +1
Scalable Verification of GNN-based Job Schedulers
Haoze Wu, Clark Barrett, Mahmood Sharif +2
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
Matan Ostrovsky, Clark Barrett, Guy Katz
DIRECT: When and Where Should You Allocate Test-Time Compute in Embodied Planners?
Jadelynn Dao, Milan Ganai, Yasmina Abukhadra +7