Sciweavers

Share
CAV
2004
Springer
126views Hardware» more  CAV 2004»
9 years 7 days ago
An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking
Model checking algorithms can report a property as being true for reasons that may be considered vacuous. Current algorithms for detecting vacuity require either checking a quadrat...
Kedar S. Namjoshi
FORMATS
2007
Springer
9 years 11 days ago
CSL Model Checking Algorithms for Infinite-State Structured Markov Chains
Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov c...
Anne Remke, Boudewijn R. Haverkort
CAV
1998
Springer
130views Hardware» more  CAV 1998»
9 years 22 days ago
On Checking Model Checkers
It has become good practice to expect authors of new model checking algorithms to provide not only rigorous evidence of the algorithms correctness, but also evidence of their pract...
Gerard J. Holzmann
RTCSA
1999
IEEE
9 years 23 days ago
Scheduling a Steel Plant with Timed Automata
Scheduling in an environment with constraints of many different types is known to be a hard problem. We tackle this problem for an integrated steel plant in Ghent, Belgium, using ...
Ansgar Fehnker
TPHOL
2003
IEEE
9 years 1 months ago
Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover
Abstract. Model checking and theorem proving are two complementary approaches to formal verification. In this paper we show how binary decision diagram (BDD) based symbolic model ...
Hasan Amjad
FORMATS
2004
Springer
9 years 1 months ago
Symbolic Model Checking for Simply-Timed Systems
Abstract. We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be a...
Nicolas Markey, Ph. Schnoebelen
ECLIPSE
2004
ACM
9 years 1 months ago
Supporting model checking education using BOGOR/Eclipse
This paper describes our effort on developing educational materials on model checking to help foster the adoption of software model checking. We describe the course materials tha...
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier
SPIN
2005
Springer
9 years 2 months ago
Model Checking Machine Code with the GNU Debugger
Embedded software verification is an important verification problem that requires the ability to reason about the timed semantics of concurrent behaviors at a low level of atomic...
Eric Mercer, Michael Jones
FMCO
2005
Springer
173views Formal Methods» more  FMCO 2005»
9 years 2 months ago
Cluster-Based LTL Model Checking of Large Systems
Abstract. In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed-memory enumerative LTL mode...
Jiri Barnat, Lubos Brim, Ivana Cerná
CHARME
2005
Springer
176views Hardware» more  CHARME 2005»
9 years 2 months ago
An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment
Abstract. Model checking is a formal technique for automatically verifying that a finite-state model satisfies a temporal property. In model checking, generally Binary Decision D...
Nina Amla, Xiaoqun Du, Andreas Kuehlmann, Robert P...
books