Name
Abstract | ||
|---|---|---|
In previous work, we presented symbolic reachability analysis by linking ProB, an animator and model checker for B and Event-B, and LTSmin, a language-independent model checker offering state-of-the-art model checking algorithms. Although the results seemed very promising, it was a very basic integration of these tools and much potential of LTSmin was not covered by the implementation.In this paper, we present a much more mature version of this tool integration. In particular, explicit-state model checking, efficient verification of state invariants, model checking of LTL properties, as well as partial order reduction and proper multi-core model checking are now available. The ( improved) performance of this advanced tool link is benchmarked on a series of models with various sizes and compared to ProB. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-98938-9_16 | INTEGRATED FORMAL METHODS, IFM 2018 |
Field | DocType | Volume |
Model checking,Programming language,Computer science,Theoretical computer science,Reachability | Conference | 11023 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
25 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Philipp Körner | 1 | 4 | 1.75 |
| Michael Leuschel | 2 | 2156 | 135.89 |
| Jeroen Meijer | 3 | 47 | 5.66 |