-
Article
Global optimization of objective functions represented by ReLU networks
Neural networks can learn complex, non-convex functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversa...
-
Chapter and Conference Paper
Efficient Neural Network Analysis with Sum-of-Infeasibilities
Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex ...
-
Article
Open AccessInterpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in pa...
-
Chapter and Conference Paper
The Marabou Framework for Verification and Analysis of Deep Neural Networks
Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that...
-
Chapter and Conference Paper
Exploring Approximations for Floating-Point Arithmetic Using UppSAT
We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT—an new implementation of a systematic approximation refinement framework [21] as an abstract SM...
-
Article
Open AccessAn Approximation Framework for Solvers and Decision Procedures
We consider the problem of automatically and efficiently computing models of constraints, in the presence of complex background theories such as floating-point arithmetic. Constructing models, or proving that ...
-
Chapter and Conference Paper
Deciding Bit-Vector Formulas with mcSAT
The Model-Constructing Satisfiability Calculus (mcSAT) is a recently proposed generalization of propositional DPLL/CDCL for reasoning modulo theories. In contrast to most DPLL(T)-based SMT solvers, which carry ou...
-
Chapter and Conference Paper
Approximations for Model Construction
We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floating-point arithmetic. Model construction has various application...
