A Decidable Logic for Tree Data-Structures with Measurements
Abstract elided by the publisher.
642 papers · page 10 of 33
On the Semantics of Snapshot Isolation
Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). It is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing …
Program Synthesis with Equivalence Reduction
Abstract elided by the publisher.
Application of Abstract Interpretation to the Automotive Electronic Control System
Abstract elided by the publisher.
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Abstract elided by the publisher.
Gradual Program Verification
Both static and dynamic program verification approaches have significant disadvantages when considered in isolation. Inspired by research on gradual typing, we propose gradual verification to seamlessly and flexibly combine static and dynamic verification. Drawing on general prin…
Automatic Verification of RMA Programs via Abstraction Extrapolation
Abstract elided by the publisher.
Scalable Approximation of Quantitative Information Flow in Programs
Abstract elided by the publisher.
Code Obfuscation Against Abstract Model Checking Attacks
Abstract elided by the publisher.
Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
Abstract elided by the publisher.
A Framework for Computer-Aided Design of Educational Domain Models
Abstract elided by the publisher.
Automatic Verification of Intermittent Systems
Abstract elided by the publisher.
On abstraction and compositionality for weak-memory linearisability
Abstract elided by the publisher.
From Shapes to Amortized Complexity
Abstract elided by the publisher.
Invariant Generation for Multi-Path Loops with Polynomial Assignments
Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properties are typically expressed as loop invariants. In this paper we study a class of multi-path program …
Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
We study cutoff results for parameterized verification and synthesis of guarded protocols, as introduced by Emerson and Kahlon (2000). Guarded protocols describe systems of processes whose transitions are enabled or disabled depending on the existence of other processes in certai…
Refinement Types for Ruby
Refinement types are a popular way to specify and reason about key program properties. In this paper, we introduce RTR, a new system that adds refinement types to Ruby. RTR is built on top of RDL, a Ruby type checker that provides basic type information for the verification proce…
Modular Analysis of Executables Using On-Demand Heyting Completion
Abstract elided by the publisher.
Learning to Complement Büchi Automata
Abstract elided by the publisher.
Co-Design and Verification of an Available File System
Abstract elided by the publisher.