Backward Symbolic Execution with Loop Folding
Abstract elided by the publisher.
783 papers · page 5 of 40
Accelerating Program Analyses in Datalog by Merging Library Facts
Abstract elided by the publisher.
Static Analysis of Endian Portability by Abstract Interpretation
Abstract elided by the publisher.
Verified Functional Programming of an Abstract Interpreter
Abstract interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their computations. While some formally verified abstract…
Disjunctive Interval Analysis
Abstract elided by the publisher.
Static Analysis of ReLU Neural Networks with Tropical Polyhedra
This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on …
Exploiting Verified Neural Networks via Floating Point Numerical Error
We show how to construct adversarial examples for neural networks with exactly verified robustness against $\ell_{\infty}$-bounded input perturbations by exploiting floating point error. We argue that any exact verification of real-valued neural networks must accurately model the…
Verifying Low-Dimensional Input Neural Networks via Input Quantization
Deep neural networks are an attractive tool for compressing the control policy lookup tables in systems such as the Airborne Collision Avoidance System (ACAS). It is vital to ensure the safety of such neural controllers via verification techniques. The problem of analyzing ACAS X…
Toward Neural-Network-Guided Program Synthesis and Verification
We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks…
Selectively-Amortized Resource Bounding
We consider the problem of automatically proving resource bounds. That is, we study how to prove that an integer-valued resource variable is bounded by a given program expression. Automatic resource-bound analysis has recently received significant attention because of a number of…
Selective Context-Sensitivity for k-CFA with CFL-Reachability
Abstract elided by the publisher.
Reduced Products of Abstract Domains for Fairness Certification of Neural Networks
Abstract elided by the publisher.
A Multilanguage Static Analysis of Python Programs with Native C Extensions
Abstract elided by the publisher.
Automated Verification of the Parallel Bellman-Ford Algorithm
Abstract elided by the publisher.
Improving Thread-Modular Abstract Interpretation
We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the…
Thread-Modular Analysis of Release-Acquire Concurrency
We present a thread-modular abstract interpretation(TMAI) technique to verify programs under the release-acquire (RA) memory model for safety property violations. The main contributions of our work are: we capture the execution order of program statements as an abstract domain, a…
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations …
Compositional Verification of Smart Contracts Through Communication Abstraction
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existing solutions either restrict the number of users to under-approximate behaviour, or rely on manual pr…
Automatic Synthesis of Data-Flow Analyzers
Abstract elided by the publisher.
Farkas-Based Tree Interpolation
Abstract elided by the publisher.