
JavaFAN
 Referenced in 29 articles
[sw01934]
 finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses ... efficient execution, search and LTL model checking of rewriting theories...

Zing
 Referenced in 38 articles
[sw01037]
 Zing is a software model checking project at Microsoft Research. Our goal is to build...

UPPAAL TIGA
 Referenced in 37 articles
[sw12913]
 Smolka [LS98] for lineartime modelchecking of finitestate systems. Being...

SatAbs
 Referenced in 36 articles
[sw12804]
 ANSIC. This paper presents a model checking tool, SatAbs, that implements a predicate abstraction ... using a SATsolver. This allows the model checker to handle the semantics...

SMART_
 Referenced in 33 articles
[sw04097]
 techniques, as well as symbolic CTL modelchecking algorithms, are available. For the study ... process, but certain classes of nonMarkov models can still be solved numerically. Finally, since...

HySAT
 Referenced in 23 articles
[sw01980]
 efficient proof engine for bounded model checking of hybrid systems n this paper we present ... that arise naturally in the bounded model checking context, e.g. isomorphic replication of learned conflict...

DiVinE
 Referenced in 32 articles
[sw04130]
 DIVINE is a tool for LTL model checking and reachability analysis of discrete distributed systems...

Pex
 Referenced in 32 articles
[sw07263]
 symbolic execution, similar to pathbounded modelchecking) to determine test inputs for Parameterized Unit...

VESTA
 Referenced in 22 articles
[sw08425]
 probabilistic systems. It supports statistical modelchecking [6, 7] and statistical evaluation of expected values ... temporal expressions. For modelchecking VESTA uses a sequence of interrelated statistical hypothesis testing ... check if a property speciﬁed in probabilistic computation tree logic (PCTL) [3] or continuous stochastic ... logic (CSL) is satisﬁed by a stochastic model. Furthermore, VESTA supports the statistical computation...

STeP
 Referenced in 30 articles
[sw17948]
 finitestate systems, but combines model checking with deductive methods to allow the verification...

PVeStA
 Referenced in 15 articles
[sw08423]
 PVeStA: A parallel statistical model checking and quantitative analysis tool. Statistical model checking ... drastically increasing the scalability of statistical model checking, and making such scalability of analysis available ... parallelization of the VeStA statistical model checking tool [10]. PVeStA supports statistical model checking ... Furthermore, the properties that it can model check can be expressed in either: (i) PCTL/CSL...

SPOT
 Referenced in 20 articles
[sw09473]
 SPOT: an extensible model checking library using transitionbased generalized Büchi automata. SPOT (SPOT produces ... traces), is a C++ library offering model checking bricks that can be combined and interfaced ... with third party tools to build a model checker. It relies on transitionbased generalized ... need to degeneralize these automata to check their emptiness. We motivate the choice of TGBA...

BPEL2oWFN
 Referenced in 27 articles
[sw06956]
 logic formula with a variety of model checking tools...

Rabbit
 Referenced in 24 articles
[sw01317]
 gives a short overview of a model checking tool for realtime systems. The modeling ... concepts for modular modeling. The tool provides reachability analysis and refinement checking, both implemented using ... computed from the modular structure of the model and an estimate of the BDD size...

Bedwyr
 Referenced in 16 articles
[sw09460]
 Bedwyr System for Model Checking over Syntactic Expressions. Bedwyr is a generalization of logic programming ... that allows model checking directly on syntactic expressions possibly containing bindings. This system, written ... sequent calculus can capture simple model checking problems as well as may and must behavior...

Romeo
 Referenced in 25 articles
[sw00812]
 modelchecking of reachability properties. It performs translations from TPNs to Timed Automata (TAs) that ... stopped and resumed, thus allowing the modeling preemption...

LIBRA
 Referenced in 25 articles
[sw10553]
 Many graphical tools are provided for model checking and outlier detection. Most of the functions...

LTSmin
 Referenced in 13 articles
[sw07214]
 LTSmin is a toolset for model checking and manipulating labelled transition systems. LTSmin already connects ... automatically yields tools for standard reachability checking (e.g., for state space generation and verification ... which exploits the combinatorial nature of model checking problems. This splits model checking tools into ... parts: language modules, PINS optimizations, and model checking algorithms. On the other hand, the implementation...

UCLID
 Referenced in 23 articles
[sw04657]
 verifier, for termlevel bounded model checking, correspondence checking, deductive verification, and predicate abstractionbased...

PGSolver
 Referenced in 23 articles
[sw14051]
 decision procedures (validity as well as model checking) for temporal logics. In this paper...