FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
We propose a model for modular synchronous systems with combinational dependencies and define consistency using this model. We then show how to derive this model from a modular spe...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
We present a symbolic algorithm for strongly connected component decomposition. The algorithm performs (n log n) image and preimage computations in the worst case, where n is the n...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly mod...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
BLIF is a hardware description language designed for the hierarchical description of sequential circuits. We give a denotational semantics for BLIF-MV, a popular dialect of BLIF, t...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. Model checking is an automated approach to the formal verification of hardware and software. To allow model checking tools to be used by the hardware or software designer...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. We consider the problem of refinement checking for asynchronous processes where refinement corresponds to stutter-closed language inclusion. Since an efficient algorithmi...
FMCAD
2000
Springer
14 years 3 months ago
2000
Springer
Abstract. We present a formal verification methodology for datapathdominated hardware. This provides a systematic but flexible framework within which to organize the activities und...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
Polygonal hybrid systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
Recently, a new approach to the symbolic model checking of timed automata based on a partial order semantics was introduced, which relies on event zones that use vectors of event o...
FORMATS
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. We show how to transform formulae written in the real-time temporal logic MITL into timed automata that recognize their satisfying models. This compositional construction...