The Power of Symbolic Automata and Transducers
Abstract elided by the publisher.
2,069 papers · page 34 of 104
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts
Abstract elided by the publisher.
A Storm is Coming: A Modern Probabilistic Model Checker
We launch the new probabilistic model checker Storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the Prism and JANI modeling languages, probabilistic programs, dynamic fault trees and generalized stochastic Petri …
Synthesis with Abstract Examples
Abstract elided by the publisher.
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
Abstract elided by the publisher.
Network-Wide Configuration Synthesis
Computer networks are hard to manage. Given a set of high-level requirements (e.g., reachability, security), operators have to manually figure out the individual configuration of potentially hundreds of devices running complex distributed protocols so that they, collectively, com…
DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems
We present the DryVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivi…
BoSy: An Experimentation Framework for Bounded Synthesis
We present \(\textsf {BoSy}\), a reactive synthesis tool based on the bounded synthesis approach. Bounded synthesis ensures the minimality of the synthesized implementation by incrementally increasing a bound on the size of the solutions it considers. For each bound, the existenc…
Efficient Parallel Strategy Improvement for Parity Games
We study strategy improvement algorithms for solving parity games. While these algorithms are known to solve parity games using a very small number of iterations, experimental studies have found that a high step complexity causes them to perform poorly in practice. In this paper …
EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties
Abstract elided by the publisher.
Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems
Abstract elided by the publisher.
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
Abstract elided by the publisher.
Verifying Equivalence of Spark Programs
Abstract elided by the publisher.
Safety Verification of Deep Neural Networks
Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential application…
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel,…
Bounded Synthesis for Streett, Rabin, and \text CTL^*
Abstract elided by the publisher.
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Abstract elided by the publisher.
Cutoff Bounds for Consensus Algorithms
Abstract elided by the publisher.
Synchronization Synthesis for Network Programs
Abstract elided by the publisher.
A Correct-by-Decision Solution for Simultaneous Place and Route
Abstract elided by the publisher.