Data-Driven Synthesis of Full Probabilistic Programs
Abstract elided by the publisher.
26,098 papers · page 454 of 1,305
Non-polynomial Worst-Case Analysis of Recursive Programs
We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to re…
Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds
We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. Several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are ei…
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT
Abstract elided by the publisher.
Lagrangian Reachabililty
We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the grad…
The Power of Symbolic Automata and Transducers
Abstract elided by the publisher.
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,…