Timing Analysis of Parallel Software Using Abstract Execution
Abstract elided by the publisher.
642 papers · page 16 of 33
Widening for Control-Flow
Abstract elided by the publisher.
Message-Passing Algorithms for the Verification of Distributed Protocols
Abstract elided by the publisher.
Probabilistic Automata for Safety LTL Specifications
Abstract elided by the publisher.
Synthesis for Polynomial Lasso Programs
We present a method for the synthesis of polynomial lasso programs. These programs consist of a program stem, a set of transitions, and an exit condition, all in the form of algebraic assertions conjunctions of polynomial equalities. Central to this approach is the discovery of n…
Weakest Precondition Synthesis for Compiler Optimizations
Abstract elided by the publisher.
Policy Iteration-Based Conditional Termination and Ranking Functions
Abstract elided by the publisher.
Relational Thread-Modular Static Value Analysis by Abstract Interpretation
Abstract elided by the publisher.
Practical Floating-Point Tests with Integer Code
Abstract elided by the publisher.
Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs
Abstract elided by the publisher.
Modular Synthesis of Sketches Using Models
One problem with the constraint-based approaches to synthesis that have become popular over the last few years is that they only scale to relatively small routines, on the order of a few dozen lines of code. This paper presents a mechanism for modular reasoning that allows us to …
Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes
In this paper we study strong and weak bisimulation equivalences for continuous-time Markov decision processes CTMDPs and the logical characterizations of these relations with respect to the continuous-time stochastic logic CSL. For strong bisimulation, it is well known that it i…
Cascade 2.0
Abstract elided by the publisher.
Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability
Abstract elided by the publisher.
All for the Price of Few
Abstract elided by the publisher.
Quantifying Information Leakage of Randomized Protocols
Abstract elided by the publisher.
An Abstract Interpretation of DPLL(T)
Abstract elided by the publisher.
Compositional Sequentialization of Periodic Programs
Abstract elided by the publisher.
Flow-Sensitive Fault Localization
Abstract elided by the publisher.
Automatic Inference of Necessary Preconditions
Abstract elided by the publisher.