An Abstraction-Refinement Framework for Trigger Querying
Abstract elided by the publisher.
783 papers · page 16 of 40
The Flow-Insensitive Precision of Andersen's Analysis in Practice
Abstract elided by the publisher.
On Sequentializing Concurrent Programs
We propose a general framework for compositional under-approximate concurrent program analyses by reduction to sequential program analyses--so-called sequentializations. We notice the existing sequentializations--based on bounding the number of execution contexts, execution round…
Software Verification Using k-Induction
Abstract elided by the publisher.
Abstract Domains of Affine Relations
Abstract elided by the publisher.
Probabilistic Abstractions with Arbitrary Domains
Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. These approaches are limited to predicate abstraction. We present a novel technique, based on the abstract reachability tree recently …
Formal Model Reduction
Modelers of molecular signaling networks must cope with the combinatorial explosion of protein states generated by post-translational modifications and complex formations. Rule-based models provide a powerful alternative to approaches that require an explicit enumeration of all p…
Side-Effect Analysis of Assembly Code
Abstract elided by the publisher.
Statically Validating Must Summaries for Incremental Compositional Dynamic Test Generation
Abstract elided by the publisher.
The Complexity of Abduction for Separated Heap Abstractions
Abstract elided by the publisher.
An Efficient Static Trace Simplification Technique for Debugging Concurrent Programs
Abstract elided by the publisher.
Astrée: Design and Experience
Abstract elided by the publisher.
Directed Symbolic Execution
Abstract elided by the publisher.
Purity Analysis: An Abstract Interpretation Formulation
Abstract elided by the publisher.
Efficient Decision Procedures for Heaps Using STRAND
Abstract elided by the publisher.
Widening and Interpolation
Abstract elided by the publisher.
Invisible Invariants and Abstract Interpretation
Abstract elided by the publisher.
A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs
We develop a framework for computing two foundational analyses for concurrent higher-order programs: (control-)flow analysis (CFA) and may-happen-in-parallel analysis (MHP). We pay special attention to the unique challenges posed by the unrestricted mixture of first-class continu…
Probabilistically Accurate Program Transformations
The standard approach to program transformation involves the use of discrete logical reasoning to prove that the transformation does not change the observable semantics of the program. We propose a new approach that, in contrast, uses probabilistic reasoning to justify the applic…
Program Analysis for Web Security
Abstract elided by the publisher.