CAV
2004
Springer
14 years 25 days ago
2004
Springer
Abstract. We present an unfolding-based approach to LTL-X modelchecking of high-level Petri nets. It is based on the method proposed by Esparza and Heljanko for low-level nets [4, ...
CAV
2004
Springer
14 years 25 days ago
2004
Springer
This paper reviews the principles behind the paradigm of “abstract interpretation via § -valued logic,” discusses recent work to extend the approach, and summarizes ongoing re...
CAV
2004
Springer
14 years 25 days ago
2004
Springer
CAV
2004
Springer
14 years 25 days ago
2004
Springer
SAL 2 augments the specification language and explicit-state model checker of SAL 1 with high-performance symbolic and bounded model checkers, and with novel infinite bounded and...
CAV
2004
Springer
14 years 25 days ago
2004
Springer
This paper presents a symbolic model checking algorithm for Fixpoint Logic with Chop, an extension of the modal µ-calculus capable of defining non-regular properties. Some empiri...
CAV
2004
Springer
14 years 25 days ago
2004
Springer
The counterexamples produced by model checkers are often lengthy and difficult to understand. In practical verification, showing the existence of a (potential) bug is not enough: ...
CAV
2004
Springer
14 years 25 days ago
2004
Springer
CAV
2004
Springer
14 years 25 days ago
2004
Springer
CAV
2004
Springer
14 years 25 days ago
2004
Springer
The logic of equality with uninterpreted functions (EUF) and its extensions have been widely applied to processor verification, by means of a large variety of progressively more s...
CAV
2004
Springer
14 years 25 days ago
2004
Springer