Foundations of Quantitative Predicate Abstraction for Stability Analysis of Hybrid Systems
Abstract elided by the publisher.
642 papers · page 15 of 33
Variations on the Stochastic Shortest Path Problem
In this invited contribution, we revisit the stochastic shortest path problem, and show how recent results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reachin…
Induction for SMT Solvers
Abstract elided by the publisher.
Distributed Markov Chains
The formal verification of large probabilistic models is challenging. Exploiting the concurrency that is often present is one way to address this problem. Here we study a class of communicating probabilistic agents in which the synchronizations determine the probability distribut…
Debugging Process Algebra Specifications
Abstract elided by the publisher.
Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation
Abstract elided by the publisher.
A Model for Industrial Real-Time Systems
Abstract elided by the publisher.
Dependent Array Type Inference from Tests
Abstract elided by the publisher.
Modeling Parsimonious Putative Regulatory Networks: Complexity and Heuristic Approach
A relevant problem in systems biology is the description of the regulatory interactions between genes. It is observed that pairs of genes have significant correlation through several experimental conditions. The question is to find causal relationships that can explain this exper…
Parameterized Model Checking of Token-Passing Systems
We revisit the parameterized model checking problem for token-passing systems and specifications in indexed CTL i?ź\X. Emerson and Namjoshi 1995, 2003 have shown that parameterized model checking of indexed CTL i?ź\X in uni-directional token rings can be reduced to checking rings…
Verifying Array Programs by Transforming Verification Conditions
Abstract elided by the publisher.
SAT-Based Synthesis Methods for Safety Specs
Automatic synthesis of hardware components from declarative specifications is an ambitious endeavor in computer aided design. Existing synthesis algorithms are often implemented with Binary Decision Diagrams BDDs, inheriting their scalability limitations. Instead of BDDs, we prop…
Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops
This paper proves the NP-completeness of the reachability problem for the class of flat counter machines with difference bounds and, more generally, octagonal relations, labeling the transitions on the loops. The proof is based on the fact that the sequence of powers $\{R^i\}_{i=…
Refuting Heap Reachability
Abstract elided by the publisher.
Doomsday Equilibria for Omega-Regular Games
Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for pe…
A Logic-Based Framework for Verifying Consensus Algorithms
Abstract elided by the publisher.
Synthesis with Identifiers
Abstract elided by the publisher.
Monitoring Parametric Temporal Logic
Abstract elided by the publisher.
Generic Combination of Heap and Value Analyses in Abstract Interpretation
Abstract elided by the publisher.
Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java
Abstract elided by the publisher.