26,098 papers · page 453 of 1,305
Pregel is a popular distributed computing model for dealing with large-scale graphs. However, it can be tricky to implement graph algorithms correctly and efficiently in Pregel’s vertex-centric model, especially when the algorithm has multiple computation stages, complicated data…
We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
In assume-guarantee synthesis, we are given a specification \(\langle A,G \rangle \), describing an assumption on the environment and a guarantee for the system, and we construct a system that interacts with an environment and is guaranteed to satisfy G whenever the environment s…
Abstract elided by the publisher.
The generation of reversible circuits from high-level code is an important problem in several application domains, including low-power electronics and quantum computing. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size …
Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficie…
Abstract elided by the publisher.
Abstract elided by the publisher.
We present a monitoring approach for verifying systems at runtime. Our approach targets systems whose components communicate with the monitors over unreliable channels, where messages can be delayed or lost. In contrast to prior works, whose property specification languages are l…
We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. Mor…
Multiphase ranking functions (\( M\varPhi \)RFs) were proposed as a means to prove the termination of a loop in which the computation progresses through a number of “phases”, and the progress of each phase is described by a different linear ranking function. Our work provides new…
Abstract elided by the publisher.
To be practically useful, modern static analyzers must precisely model the effect of both, statements in the programming language as well as frameworks used by the program under analysis. While important, manually addressing these challenges is difficult for at least two reasons:…
Linearizability is the standard correctness criterion for concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation. Proving linearizability requires identifying…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.