A Conference Management System with Verified Document Confidentiality
Abstract elided by the publisher.
2,069 papers · page 44 of 104
SMT-Based Model Checking for Recursive Programs
Abstract elided by the publisher.
Causal Termination of Multi-threaded Programs
Abstract elided by the publisher.
Proving Non-termination Using Max-SMT
Abstract elided by the publisher.
Shape Analysis via Second-Order Bi-Abduction
We present a new modular shape analysis that can synthesize heap memory specification on a per method basis. We rely on a second-order biabduction mechanism that can give interpretations to unknown shape predicates. There are several novel features in our shape analysis. Firstly,…
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction
Abstract elided by the publisher.
Automatic Atomicity Verification for Clients of Concurrent Data Structures
Abstract elided by the publisher.
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
Abstract elided by the publisher.
Symbolic Resource Bound Inference for Functional Programs
Abstract elided by the publisher.
Lazy Annotation Revisited
Abstract elided by the publisher.
Bit-Vector Rewriting with Automatic Rule Generation
Abstract elided by the publisher.
Solving Games without Controllable Predecessor
Abstract elided by the publisher.
Analyzing and Synthesizing Genomic Logic Functions
Abstract elided by the publisher.
Automating Separation Logic with Trees and Data
Abstract elided by the publisher.
SMACK: Decoupling Source Language Details from Verifier Implementations
Abstract elided by the publisher.
LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes
Abstract elided by the publisher.
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
We present the first scalable bound analysis that achieves amortized complexity analysis. In contrast to earlier work, our bound analysis is not based on general purpose reasoners such as abstract interpreters, software model checkers or computer algebra tools. Rather, we derive …
A Nonlinear Real Arithmetic Fragment
Abstract elided by the publisher.
Monadic Decomposition
Abstract elided by the publisher.
Interpolating Property Directed Reachability
Abstract elided by the publisher.