Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Abstract elided by the publisher.
642 papers · page 12 of 33
Stabilizing Floating-Point Programs Using Provenance Analysis
Abstract elided by the publisher.
Dynamic Reductions for Model Checking Concurrent Software
Symbolic model checking of parallel programs stands and falls with effective methods of dealing with the explosion of interleavings. We propose a dynamic reduction technique to avoid unnecessary interleavings. By extending Lipton’s original work with a notion of bisimilarity, we …
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability game…
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Abstract elided by the publisher.
Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT
Abstract elided by the publisher.
Solving Nonlinear Integer Arithmetic with MCSAT
Abstract elided by the publisher.
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Abstract elided by the publisher.
Efficient Elimination of Redundancies in Polyhedra by Raytracing
Abstract elided by the publisher.
Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
Abstract elided by the publisher.
Detecting All High-Level Dataraces in an RTOS Kernel
Abstract elided by the publisher.
Reachability for Dynamic Parametric Processes
In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is deci…
Conjunctive Abstract Interpretation Using Paramodulation
Abstract elided by the publisher.
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
Separation Logic (\(\mathsf {SL}\)) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order \(\mathsf {SL}\) restricted to the Bernays-Schonfinke…
Finding Relevant Templates via the Principal Component Analysis
Abstract elided by the publisher.
Sound Bit-Precise Numerical Domains
Abstract elided by the publisher.
IC3 - Flipping the E in ICE
Abstract elided by the publisher.
Viper: A Verification Infrastructure for Permission-Based Reasoning
Abstract elided by the publisher.
Tight Cutoffs for Guarded Protocols with Fairness
Guarded protocols were introduced in a seminal paper by Emerson and Kahlon 2000, and describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certain local states. We study parameterized model checking and synthesis …
Predicate Abstraction for Linked Data Structures
We present Alias Refinement Types Art, a new approach that uses predicate-abstraction to automate the verification of correctness properties of linked data structures. While there are many techniques for checking that a heap-manipulating program adheres to its specification, they…