research
∙
08/28/2023
Identifying and Mitigating the Security Risks of Generative AI
Every major technical invention resurfaces the dual-use dilemma – the ne...
share
research
∙
08/24/2023
PEak: A Single Source of Truth for Hardware Design and Verification
Domain-specific languages for hardware can significantly enhance designe...
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...
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...
research
∙
06/08/2023
Partitioning Strategies for Distributed SMT Solving
For many users of Satisfiability Modulo Theories (SMT) solvers, the solv...
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...
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...
research
∙
05/10/2023
DNN Verification, Reachability, and the Exponential Function Problem
Deep neural networks (DNNs) are increasingly being deployed to perform s...
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...
research
∙
03/23/2023
Soy: An Efficient MILP Solver for Piecewise-Affine Systems
Piecewise-affine (PWA) systems are widely used for modeling and control ...
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 (...
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...
research
∙
12/02/2022
VeriX: Towards Verified Explainability of Deep Neural Networks
We present VeriX, a first step towards verified explainability of machin...
research
∙
10/23/2022
Tighter Abstract Queries in Neural Network Verification
Neural networks have become critical components of reactive systems in v...
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...
research
∙
08/16/2022
On Optimizing Back-Substitution Methods for Neural Network Verification
With the increasing application of deep learning in mission-critical sys...
research
∙
06/01/2022
Neural Network Verification with Proof Production
Deep neural networks (DNNs) are increasingly being employed in safety-cr...
research
∙
05/17/2022
Reasoning About Vectors using an SMT Theory of Sequences
Dynamic arrays, also referred to as vectors, are fundamental data struct...
research
∙
03/19/2022
Efficient Neural Network Analysis with Sum-of-Infeasibilities
Inspired by sum-of-infeasibilities methods in convex optimization, we pr...
research
∙
03/07/2022
Scalable Verification of GNN-based Job Schedulers
Recently, Graph Neural Networks (GNNs) have been applied for scheduling ...
research
∙
01/06/2022
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
Convolutional neural networks have gained vast popularity due to their e...
research
∙
08/12/2021
Automating System Configuration
The increasing complexity of modern configurable systems makes it critic...
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...
research
∙
05/07/2021
lazybvtoint at the SMT Competition 2020
lazybvtoint is a new prototype SMT-solver, that will participate in the ...
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...
research
∙
04/23/2021
Politeness and Stable Infiniteness: Stronger Together
We make two contributions to the study of polite combination in satisfia...
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...
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...
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...
research
∙
10/07/2020
Global Optimization of Objective Functions Represented by ReLU Networks
Neural networks (NN) learn complex non-convex functions, making them des...
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...
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,...
research
∙
06/09/2020
A Theoretical Framework for Symbolic Quick Error Detection
Symbolic quick error detection (SQED) is a formal pre-silicon verificati...
research
∙
04/17/2020
Parallelization Techniques for Verifying Neural Networks
Inspired by recent successes with parallel optimization techniques for s...
research
∙
04/09/2020
Politeness for the Theory of Algebraic Datatypes
Algebraic datatypes, and among them lists and trees, have attracted a lo...
research
∙
04/06/2020
Verifying Recurrent Neural Networks using Invariant Inference
Deep neural networks are revolutionizing the way complex systems are dev...
research
∙
10/29/2019
G2SAT: Learning to Generate SAT Formulas
The Boolean Satisfiability (SAT) problem is the canonical NP-complete pr...
research
∙
10/25/2019
Simplifying Neural Networks with the Marabou Verification Engine
Deep neural network (DNN) verification is an emerging field, with divers...
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...
research
∙
07/23/2019
CVC4SY for SyGuS-COMP 2019
CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term...
research
∙
06/28/2019
DRAT-based Bit-Vector Proofs in CVC4
Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for t...
research
∙
05/24/2019
Towards Bit-Width-Independent Proofs in SMT Solvers
Many SMT solvers implement efficient SAT-based procedures for solving fi...
research
∙
03/15/2019
Algorithms for Verifying Deep Neural Networks
Deep neural networks are widely used for nonlinear function approximatio...
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...
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...
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...
research
∙
04/13/2018
On Solving Quantified Bit-Vectors using Invertibility Conditions
We present a novel approach for solving quantified bit-vector formulas i...
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...
research
∙
01/18/2018
Toward Scalable Verification for Safety-Critical Deep Networks
The increasing use of deep neural networks for safety-critical applicati...
research
∙
11/15/2017
