Sciweavers

FM
2001
Springer
118views Formal Methods» more  FM 2001»
13 years 9 months ago
Avoiding State Explosion for Distributed Systems with Timestamps
This paper describes a reduction technique which is very useful against the state explosion problem which occurs when model checking many distributed systems. Timestamps are often ...
Fabrice Derepas, Paul Gastin, David Plainfoss&eacu...
FORMATS
2004
Springer
13 years 10 months ago
Bounded Model Checking for Region Automata
For successful software verification, model checkers must be capable of handling a large number of program variables. Traditional, BDD-based model checking is deficient in this reg...
Fang Yu, Bow-Yaw Wang, Yao-Wen Huang
CAV
2004
Springer
123views Hardware» more  CAV 2004»
13 years 10 months ago
SAL 2
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...
Leonardo Mendonça de Moura, Sam Owre, Haral...
SPIN
2005
Springer
13 years 10 months ago
Symbolic Model Checking for Asynchronous Boolean Programs
Abstract. Software model checking problems generally contain two different types of non-determinism: 1) non-deterministically chosen values; 2) the choice of interleaving among th...
Byron Cook, Daniel Kroening, Natasha Sharygina
ICFEM
2005
Springer
13 years 10 months ago
An Evidential Tool Bus
Abstract. Theorem provers, model checkers, static analyzers, test generators. . . all of these and many other kinds of formal methods tools can contribute to the analysis and devel...
John M. Rushby
HVC
2007
Springer
108views Hardware» more  HVC 2007»
13 years 10 months ago
How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison
Abstract. This paper studies the efficiency of several probabilistic model checkers by comparing verification times and peak memory usage for a set of standard case studies. The s...
David N. Jansen, Joost-Pieter Katoen, Marcel Olden...