Probabilistic Program Analysis with Martingales
Abstract elided by the publisher.
2,069 papers · page 46 of 104
A Scalable and Nearly Uniform Generator of SAT Witnesses
Functional verification constitutes one of the most challenging tasks in the development of modern hardware systems, and simulation-based verification techniques dominate the functional verification landscape. A dominant paradigm in simulation-based verification is directed rando…
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In th…
Faster Algorithms for Markov Decision Processes with Low Treewidth
We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both t…
Flow*: An Analyzer for Non-linear Hybrid Systems
Abstract elided by the publisher.
JBernstein: A Validity Checker for Generalized Polynomial Constraints
Abstract elided by the publisher.
Lengths May Break Privacy - Or How to Check for Equivalences with Length
Abstract elided by the publisher.
A Tool for Estimating Information Leakage
Abstract elided by the publisher.
Model-Checking Signal Transduction Networks through Decreasing Reachability Sets
Abstract elided by the publisher.
Towards Distributed Software Model-Checking Using Decision Diagrams
Abstract elided by the publisher.
Equivalence of Extended Symbolic Finite Transducers
Abstract elided by the publisher.
Generating Non-linear Interpolants by Semidefinite Programming
Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model checking, CEGAR, SMT, etc., in which the hardest part is how to synthesize interpolants. Various work for discovering interpolants for pro…
Explain: A Tool for Performing Abductive Inference
Abstract elided by the publisher.
Efficient Robust Monitoring for STL
Abstract elided by the publisher.
Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates
Abstract elided by the publisher.
Parameterized Verification of Asynchronous Shared-Memory Systems
Abstract elided by the publisher.
A Fully Verified Executable LTL Model Checker
Abstract elided by the publisher.
Program Repair without Regret
Abstract elided by the publisher.
Duet: Static Analysis for Unbounded Parallelism
Abstract elided by the publisher.
Proving Termination Starting from the End
We present a novel technique for proving program termination which introduces a new dimension of modularity. Existing techniques use the program to incrementally construct a termination proof. While the proof keeps changing, the program remains the same. Our technique goes a step…