Abstract Interpretation of CTL Properties
Abstract elided by the publisher.
783 papers · page 9 of 40
Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction
Abstract elided by the publisher.
Probabilistic Horn Clause Verification
Abstract elided by the publisher.
Combining Forward and Backward Abstract Interpretation of Horn Clauses
Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of some undesired program states. The current state-of-the-art technique for combining forward (bottom-u…
Abstract Semantic Diffing of Evolving Concurrent Programs
Abstract elided by the publisher.
Learning Shape Analysis
Abstract elided by the publisher.
Verifying Array Manipulating Programs by Tiling
Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a novel property-driven verification method that first infers array access patterns in loops using sim…
Securing the SSA Transform
Abstract elided by the publisher.
Relative Store Fragments for Singleton Abstraction
Abstract elided by the publisher.
Loop Invariants from Counterexamples
Abstract elided by the publisher.
Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration
Abstract elided by the publisher.
A Context-Sensitive Memory Model for Verification of C/C++ Programs
Abstract elided by the publisher.
Effect Summaries for Thread-Modular Analysis - Sound Analysis Despite an Unsound Heuristic
We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates for stateless effect summaries of programs by searching the code for instances of a copy-and-check …
Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models
Abstract elided by the publisher.
Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming
Abstract elided by the publisher.
Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification
Abstract elided by the publisher.
Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
Abstract elided by the publisher.
Quantitative Static Analysis of Communication Protocols Using Abstract Markov Chains
Abstract elided by the publisher.
Template Polyhedra with a Twist
Abstract elided by the publisher.
A New Abstraction Framework for Affine Transformers
Abstract elided by the publisher.