Automatic Generation of Propagation Complete SAT Encodings
Abstract elided by the publisher.
642 papers · page 13 of 33
Model Checking with Multi-threaded IC3 Portfolios
Abstract elided by the publisher.
A General Modular Synthesis Problem for Pushdown Systems
Abstract elided by the publisher.
Abstraction-driven Concolic Testing
Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abst…
Parameter Synthesis for Parametric Interval Markov Chains
Abstract elided by the publisher.
A Program Logic for C11 Memory Fences
Abstract elided by the publisher.
From Low-Level Pointers to High-Level Containers
We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the containers are manipulated via calls of standard high-level container operations like push_back or pop_front. The input of our method is…
An Abstract Domain of Uninterpreted Functions
Abstract elided by the publisher.
Lazy Constrained Monotonic Abstraction
Abstract elided by the publisher.
Reward-Bounded Reachability Probability for Uncertain Weighted MDPs
Abstract elided by the publisher.
Pointer Race Freedom
We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results. 1 Under …
Lipschitz Robustness of Timed I/O Systems
We present the first study of robustness of systems that are both timed as well as reactive I/O. We study the behavior of such timed I/O systems in the presence of uncertain inputs and formalize their robustness using the analytic notion of Lipschitz continuity: a timed I/O syste…
Exact Heap Summaries for Symbolic Execution
Abstract elided by the publisher.
Cloud-Based Verification of Concurrent Software
Abstract elided by the publisher.
Program Analysis with Local Policy Iteration
We present local policy iterationi¾?LPI, a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis CPA framework,…
Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis
We extend abstract interpretation for the purpose of verifying hybrid systems. Abstraction has been playing an important role in many verification methodologies for hybrid systems, but some special care is needed for abstraction of continuous dynamics defined by ODEs. We apply Co…
Regular Symmetry Patterns
Abstract elided by the publisher.
Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem
Abstract elided by the publisher.
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
Abstract elided by the publisher.
D^3 : Data-Driven Disjunctive Abstraction
Abstract elided by the publisher.