Compositional Synthesis of Reactive Controllers for Multi-agent Systems
Abstract elided by the publisher.
2,069 papers · page 36 of 104
Markov Chains and Unambiguous Büchi Automata
Abstract elided by the publisher.
Synthesizing Probabilistic Invariants via Doob's Decomposition
When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then apply the optional stopping theorem in order to infer properties at termination time. One of the ma…
Solving Parity Games via Priority Promotion
Abstract elided by the publisher.
Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems
Fault-tolerant distributed algorithms play an increasingly important role in many applications, and their correct and efficient implementation is notoriously difficult. We present an automatic approach to synthesise provably correct fault-tolerant distributed algorithms from form…
Symbolic Optimal Reachability in Weighted Timed Automata
Weighted timed automata have been defined in the early 2000 s for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. …
The Kind 2 Model Checker
Abstract elided by the publisher.
Termination Analysis of Probabilistic Programs Through Positivstellensatz's
We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of …
The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach
MapReduce is a popular programming model for data parallel computation. In MapReduce, the reducer produces an output from a list of inputs. Due to the scheduling policy of the platform, the inputs may arrive at the reducers in different order. The commutativity problem of reducer…
Structural Synthesis for GXW Specifications
We define the \(\textsf {\small {GXW}} \) fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since \(\textsf {\small {GXW}} \) includes the use of a weak-until operator we are able to specify a number …
Hitting Families of Schedules for Asynchronous Programs
We consider the following basic task in the testing of concurrent systems. The input to the task is a partial order of events, which models actions performed on or by the system and specifies ordering constraints between them. The task is to determine if some scheduling of these …
A Decision Procedure for Sets, Binary Relations and Partial Functions
Abstract elided by the publisher.
Qlose: Program Repair with Quantitative Objectives
Abstract elided by the publisher.
Array Folds Logic
We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as “the first array cell contains the array length,” and “the array contains equally many min…
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
Abstract elided by the publisher.
Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances
Abstract elided by the publisher.
Effectively Propositional Interpolants
Abstract elided by the publisher.
Parsimonious, Simulation Based Verification of Linear Systems
Abstract elided by the publisher.
Slugs: Extensible GR(1) Synthesis
Abstract elided by the publisher.
Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits
Abstract elided by the publisher.