Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016)
Abstract elided by the publisher.
1,553 papers · page 34 of 78
The xSAP Safety Analysis Platform
This paper describes the xSAP safety analysis platform. xSAP provides several model-based safety analysis features for finite- and infinite-state synchronous transition systems. In particular, it supports library-based definition of fault modes, an automatic model extension facil…
Complementing Semi-deterministic Büchi Automata
Abstract elided by the publisher.
Approaching the Coverability Problem Continuously
The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this probl…
Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities
Abstract elided by the publisher.
T2: Temporal Property Verification
We present the open-source tool T2, the first public release from the TERMINATOR projecti??[9]. T2 has been extended over the past decade to support automatic temporal-logic proving techniques and to handle a general class of user-provided liveness and safety properties. Input ca…
FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals
Abstract elided by the publisher.
Efficient Syntax-Driven Lumping of Differential Equations
We present an algorithm to compute exact aggregations of a class of systems of ordinary differential equations ODEs. Our approach consists in an extension of Paige and Tarjan's seminal solution to the coarsest refinement problem by encoding an ODE system into a suitable discrete-…
PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems
Abstract elided by the publisher.
Deductive Proofs of Almost Sure Persistence and Recurrence Properties
Abstract elided by the publisher.
Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution)
Abstract elided by the publisher.
Parametric Runtime Verification of C Programs
Many runtime verification tools are built based on Aspect-Oriented Programming (AOP) tools, most often AspectJ, a mature implementation of AOP for Java. Although already popular in the Java domain, there is few work on runtime verification of C programs via AOP, due to the lack o…
Integrated Environment for Diagnosing Verification Errors
Abstract elided by the publisher.
Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-Sensitive Business Processes
Abstract elided by the publisher.
Faster Statistical Model Checking for Unbounded Temporal Properties
We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly con…
Runtime Monitoring with Union-Find Structures
Abstract elided by the publisher.
Multi-core Symbolic Bisimulation Minimisation
Abstract elided by the publisher.
Probabilistic CTL*: The Deductive Way
Complex probabilistic temporal behaviours need to be guaranteed in robotics and various other control domains, as well as in the context of families of randomized protocols. At its core, this entails checking infinite-state probabilistic systems with respect to quantitative prope…
On Atomicity in Presence of Non-atomic Writes
Abstract elided by the publisher.
DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
Abstract elided by the publisher.