2,069 papers · page 42 of 104
We present a new framework for modular verification of hardware designs in the style of the Bluespec language. That is, we formalize the idea of components in a hardware design, with well-defined input and output channels; and we show how to specify and verify components individu…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
In this paper we address the synthesis problem for specifications given in linear temporal single-agent epistemic logic, KLTL (or KL 1), over single-agent systems having imperfect information of the environment state. [17] have shown that this problem is 2Exptime complete. Howeve…
A standard approach to optimizing long-run running costs of discrete systems is based on minimizing the mean-payoff, i.e., the long-run average amount of resources ("energy") consumed per transition. However, this approach inherently assumes that the energy source has an unbounde…
Abstract elided by the publisher.
Model checking has come of age. A number of techniques are increasingly used in industrial setting to verify hardware and software systems, both against models and concrete implementations. While it is generally accepted that obstacles still remain, notably handling infinite stat…
While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in for repair process. These include reordering of instru…
We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a…
G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and t…