Function Pointer Eliminator for C Programs
Abstract elided by the publisher.
26,098 papers · page 265 of 1,305
Proving LTL Properties of Bitvector Programs and Decompiled Binaries
There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approxi…
A Compilation Method for Dynamic Typing in ML
Abstract elided by the publisher.
Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination
We propose an automated method for proving termination of $\pi$-calculus processes, based on a reduction to termination of sequential programs: we translate a $\pi$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can …
A Dictionary-Passing Translation of Featherweight Go
The Go programming language is an increasingly popular language but some of its features lack a formal investigation. This article explains Go's resolution mechanism for overloaded methods and its support for structural subtyping by means of translation from Featherweight Go …
Simplifying Alternating Automata for Emptiness Testing
Abstract elided by the publisher.
Scalable and Modular Robustness Analysis of Deep Neural Networks
As neural networks are trained to be deeper and larger, the scalability of neural network analyzers is urgently required. The main technical insight of our method is modularly analyzing neural networks by segmenting a network into blocks and conduct the analysis for each block. I…
Learning Probabilistic Termination Proofs
Abstract We present the first machine learning approach to the termination analysis of probabilistic programs. Ranking supermartingales (RSMs) prove that probabilistic programs halt, in expectation, within a finite number of steps. While previously RSMs were directly synthesised …
Stateless Model Checking Under a Reads-Value-From Equivalence
Abstract Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explor…
Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata
Abstract Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed automata with a, possibly unbounded, stack, also called pushdown timed automata (PDTA). While d…
Lower-Bound Synthesis Using Loop Specialization and Max-SMT
Abstract This paper presents a new framework to synthesize lower-bounds on the worst-case cost for non-deterministic integer loops. As in previous approaches, the analysis searches for a metering function that under-approximates the number of loop iterations. The key novelty of o…
Adapting Behaviors via Reactive Synthesis
Abstract In the Adapter Design Pattern, a programmer implements a Target interface by constructing an Adapter that accesses an existing Adaptee code. In this work, we present a reactive synthesis interpretation to the adapter design pattern, wherein an algorithm takes an Adaptee …
IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability
Abstract Real-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satis…
PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs
Abstract This paper presents PAYNT, a tool to automatically synthesise probabilistic programs. PAYNT enables the synthesis of finite-state probabilistic programs from a program sketch representing a finite family of program candidates. A tight interaction between inductive oracle…
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models
Abstract Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hither…
JavaSMT 3: Interacting with SMT Solvers in Java
Abstract Satisfiability Modulo Theories (SMT) is an enabling technology with many applications, especially in computer-aided verification. Due to advances in research and strong demand for solvers, there are many SMT solvers available. Since different implementations have differe…
Causality-Based Game Solving
Abstract We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. Our technique for solving these games is based o…
Latticed k-Induction with an Application to Probabilistic Programs
Abstract We revisit two well-established verification techniques,k-inductionandbounded model checking(BMC), in the more general setting of fixed point theory over complete lattices. Our main theoretical contribution islatticed k-induction, which (i) generalizes classicalk-inducti…
A Temporal Logic for Asynchronous Hyperproperties
Abstract Hyperpropertiesare properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The te…
Debugging Network Reachability with Blocked Paths
Abstract In this industrial case study we describe a new network troubleshooting analysis used by VPC Reachability Analyzer , an SMT-based network reachability analysis and debugging tool. Our troubleshooting analysis uses a formal model of AWS Virtual Private Cloud (VPC) semanti…