b'Clark Barrett'

research

∙ 08/28/2023

Identifying and Mitigating the Security Risks of Generative AI

Every major technical invention resurfaces the dual-use dilemma – the ne...

0 Clark Barrett, et al. ∙

research

∙ 08/24/2023

PEak: A Single Source of Truth for Hardware Design and Verification

Domain-specific languages for hardware can significantly enhance designe...

0 Caleb Donovick, et al. ∙

research

∙ 07/15/2023

Combining Finite Combination Properties: Finite Models and Busy Beavers

This work is a part of an ongoing effort to understand the relationships...

0 Guilherme Toledo, et al. ∙

research

∙ 06/24/2023

H_2O: Heavy-Hitter Oracle for Efficient Generative Inference of Large Language Models

Large Language Models (LLMs), despite their recent impressive accomplish...

0 Zhenyu Zhang, et al. ∙

research

∙ 06/08/2023

Partitioning Strategies for Distributed SMT Solving

For many users of Satisfiability Modulo Theories (SMT) solvers, the solv...

0 Amalee Wilson, et al. ∙

research

∙ 06/03/2023

On Optimal Caching and Model Multiplexing for Large Model Inference

Large Language Models (LLMs) and other large foundation models have achi...

0 Banghua Zhu, et al. ∙

research

∙ 05/18/2023

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning

We present Self-Driven Strategy Learning (sdsl), a lightweight online le...

0 Haoze Wu, et al. ∙

research

∙ 05/10/2023

DNN Verification, Reachability, and the Exponential Function Problem

Deep neural networks (DNNs) are increasingly being deployed to perform s...

0 Omri Isac, et al. ∙

research

∙ 05/03/2023

Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness

We make two contributions to the study of theory combination in satisfia...

0 Guilherme Vicentin de Toledo, et al. ∙

research

∙ 03/23/2023

Soy: An Efficient MILP Solver for Piecewise-Affine Systems

Piecewise-affine (PWA) systems are widely used for modeling and control ...

0 Haoze Wu, et al. ∙

research

∙ 03/13/2023

FlexGen: High-Throughput Generative Inference of Large Language Models with a Single GPU

The high computational and memory requirements of large language model (...

0 Ying Sheng, et al. ∙

research

∙ 03/03/2023

Convex Bounds on the Softmax Function with Applications to Robustness Verification

The softmax function is a ubiquitous component at the output of neural n...

0 Dennis Wei, et al. ∙

research

∙ 12/02/2022

VeriX: Towards Verified Explainability of Deep Neural Networks

We present VeriX, a first step towards verified explainability of machin...

0 Min Wu, et al. ∙

research

∙ 10/23/2022

Tighter Abstract Queries in Neural Network Verification

Neural networks have become critical components of reactive systems in v...

0 Elazar Cohen, et al. ∙

research

∙ 09/04/2022

Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers

With the increasing availability of parallel computing power, there is a...

0 Abhishek Nair, et al. ∙

research

∙ 08/16/2022

On Optimizing Back-Substitution Methods for Neural Network Verification

With the increasing application of deep learning in mission-critical sys...

0 Tom Zelazny, et al. ∙

research

∙ 06/01/2022

Neural Network Verification with Proof Production

Deep neural networks (DNNs) are increasingly being employed in safety-cr...

0 Omri Isac, et al. ∙

research

∙ 05/17/2022

Reasoning About Vectors using an SMT Theory of Sequences

Dynamic arrays, also referred to as vectors, are fundamental data struct...

0 Ying Sheng, et al. ∙

research

∙ 03/19/2022

Efficient Neural Network Analysis with Sum-of-Infeasibilities

Inspired by sum-of-infeasibilities methods in convex optimization, we pr...

49 Haoze Wu, et al. ∙

research

∙ 03/07/2022

Scalable Verification of GNN-based Job Schedulers

Recently, Graph Neural Networks (GNNs) have been applied for scheduling ...

0 Haoze Wu, et al. ∙

research

∙ 01/06/2022

An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks

Convolutional neural networks have gained vast popularity due to their e...

0 Matan Ostrovsky, et al. ∙

research

∙ 08/12/2021

Automating System Configuration

The increasing complexity of modern configurable systems makes it critic...

0 Nestan Tsiskaridze, et al. ∙

research

∙ 06/18/2021

Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection

We present a novel approach to pre-silicon verification of processor des...

0 Karthik Ganesan, et al. ∙

research

∙ 05/07/2021

lazybvtoint at the SMT Competition 2020

lazybvtoint is a new prototype SMT-solver, that will participate in the ...

0 Yoni Zohar, et al. ∙

research

∙ 04/29/2021

Automated Design Space Exploration of CGRA Processing Element Architectures using Frequent Subgraph Analysis

The architecture of a coarse-grained reconfigurable array (CGRA) process...

0 Jackson Melchert, et al. ∙

research

∙ 04/23/2021

Politeness and Stable Infiniteness: Stronger Together

We make two contributions to the study of polite combination in satisfia...

0 Ying Sheng, et al. ∙

research

∙ 03/02/2021

DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers

We introduce DeepCert, a tool-supported method for verifying the robustn...

0 Colin Paterson, et al. ∙

research

∙ 01/18/2021

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

We develop a framework for model checking infinite-state systems by auto...

0 Makai Mann, et al. ∙

research

∙ 11/05/2020

An SMT-Based Approach for Verifying Binarized Neural Networks

Deep learning has emerged as an effective approach for creating modern s...

0 Guy Amir, et al. ∙

research

∙ 10/07/2020

Global Optimization of Objective Functions Represented by ReLU Networks

Neural networks (NN) learn complex non-convex functions, making them des...

0 Christopher A. Strong, et al. ∙

research

∙ 07/02/2020

Smt-Switch: a solver-agnostic C++ API for SMT Solving

This extended abstract describes work in progress on Smt-Switch, an open...

0 Makai Mann, et al. ∙

research

∙ 06/20/2020

fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components

While hardware generators have drastically improved design productivity,...

0 Lenny Truong, et al. ∙

research

∙ 06/09/2020

A Theoretical Framework for Symbolic Quick Error Detection

Symbolic quick error detection (SQED) is a formal pre-silicon verificati...

0 Florian Lonsing, et al. ∙

research

∙ 04/17/2020

Parallelization Techniques for Verifying Neural Networks

Inspired by recent successes with parallel optimization techniques for s...

0 Haoze Wu, et al. ∙

research

∙ 04/09/2020

Politeness for the Theory of Algebraic Datatypes

Algebraic datatypes, and among them lists and trees, have attracted a lo...

0 Ying Sheng, et al. ∙

research

∙ 04/06/2020

Verifying Recurrent Neural Networks using Invariant Inference

Deep neural networks are revolutionizing the way complex systems are dev...

5 Yuval Jacoby, et al. ∙

research

∙ 10/29/2019

G2SAT: Learning to Generate SAT Formulas

The Boolean Satisfiability (SAT) problem is the canonical NP-complete pr...

6 Jiaxuan You, et al. ∙

research

∙ 10/25/2019

Simplifying Neural Networks with the Marabou Verification Engine

Deep neural network (DNN) verification is an emerging field, with divers...

0 Sumathi Gokulanathan, et al. ∙

research

∙ 08/26/2019

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)

This work is a part of an ongoing effort to prove the correctness of inv...

0 Burak Ekici, et al. ∙

research

∙ 07/23/2019

CVC4SY for SyGuS-COMP 2019

CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term...

0 Andrew Reynolds, et al. ∙

research

∙ 06/28/2019

DRAT-based Bit-Vector Proofs in CVC4

Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for t...

0 Alex Ozdemir, et al. ∙

research

∙ 05/24/2019

Towards Bit-Width-Independent Proofs in SMT Solvers

Many SMT solvers implement efficient SAT-based procedures for solving fi...

0 Aina Niemetz, et al. ∙

research

∙ 03/15/2019

Algorithms for Verifying Deep Neural Networks

Deep neural networks are widely used for nonlinear function approximatio...

0 Changliu Liu, et al. ∙

research

∙ 02/04/2019

Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study

We present an industrial case study that demonstrates the practicality a...

0 Eshan Singh, et al. ∙

research

∙ 12/05/2018

Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking

Recent discovery of security attacks in advanced processors, known as Sp...

0 Mohammad Rahmani Fadiheh, et al. ∙

research

∙ 06/20/2018

CVC4 at the SMT Competition 2018

This paper is a description of the CVC4 SMT solver as entered into the 2...

0 Clark Barrett, et al. ∙

research

∙ 04/13/2018

On Solving Quantified Bit-Vectors using Invertibility Conditions

We present a novel approach for solving quantified bit-vector formulas i...

0 Aina Niemetz, et al. ∙

research

∙ 01/30/2018

EMME: a formal tool for ECMAScript Memory Model Evaluation

Nearly all web-based interfaces are written in JavaScript. Given its pre...

0 Cristian Mattarei, et al. ∙

research

∙ 01/18/2018

Toward Scalable Verification for Safety-Critical Deep Networks

The increasing use of deep neural networks for safety-critical applicati...

0 Lindsey Kuper, et al. ∙

research

∙ 11/15/2017

Logic Bug Detection and Localization Using Symbolic Quick Error Detection

We present Symbolic Quick Error Detection (Symbolic QED), a structured a...

0 Eshan Singh, et al. ∙

Clark Barrett

Featured Co-authors