119 citations · 465 across the 38 of their papers we have counts for
9 papers · 1 filter
An SMT-Based Approach for Verifying Binarized Neural Networks
Guy Amir, Haoze Wu, Clark Barrett +1
Deep learning has emerged as an effective approach for creating modern software systems, with neural networks often surpassing hand-crafted systems. Unfortunately, neural networks…
Global Optimization of Objective Functions Represented by ReLU Networks
Christopher A. Strong, Haoze Wu, Aleksandar Zeljić +4
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 failur…
Smt-Switch: a solver-agnostic C++ API for SMT Solving
Makai Mann, Amalee Wilson, Cesare Tinelli +1
This extended abstract describes work in progress on Smt-Switch, an open-source, solver-agnostic API for SMT solving. Smt-Switch provides an abstract interface, which can be implem…
fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
Lenny Truong, Steven Herbst, Rajsekhar Setaluri +8
While hardware generators have drastically improved design productivity, they have introduced new challenges for the task of verification. To effectively cover the functionality of…
A Theoretical Framework for Symbolic Quick Error Detection
Florian Lonsing, Subhasish Mitra, Clark Barrett
Symbolic quick error detection (SQED) is a formal pre-silicon verification technique targeted at processor designs. It leverages bounded model checking (BMC) to check a design for…
Politeness for the Theory of Algebraic Datatypes
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable versi…
Parallelization Techniques for Verifying Neural Networks
Haoze Wu, Alex Ozdemir, Aleksandar Zeljić +7
Inspired by recent successes with parallel optimization techniques for solving Boolean satisfiability, we investigate a set of strategies and heuristics that aim to leverage parall…
Resources: A Safe Language Abstraction for Money
Sam Blackshear, David L. Dill, Shaz Qadeer +4
Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract pr…
Verifying Recurrent Neural Networks using Invariant Inference
Yuval Jacoby, Clark Barrett, Guy Katz
Deep neural networks are revolutionizing the way complex systems are developed. However, these automatically-generated networks are opaque to humans, making it difficult to reason…