
Bandera
 Referenced in 134 articles
[sw07663]
 Using the Bandera tool set to modelcheck properties of concurrent Java software. The Bandera ... components designed to facilitate experimentation with modelchecking Java source code. Bandera takes as input ... language of one of several existing modelchecking tools (including Spin, dSpin ... model to the property being checked. When a modelchecker produces an error trail, Bandera...

SLMC
 Referenced in 72 articles
[sw04604]
 model checking concurrent systems against dynamical spatial logic specifications. The Spatial Logic Model Checker ... concurrency of Caires and Cardelli. Modelchecking is one of the most widely used techniques...

CMC
 Referenced in 34 articles
[sw12422]
 Tool for Compositional ModelChecking of RealTime Systems. In this paper we present ... tool (CMC) for compositional modelchecking of realtime systems. CMC is based...

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

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

VESTA
 Referenced in 24 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...

SMART_
 Referenced in 33 articles
[sw04097]
 techniques, as well as symbolic CTL modelchecking algorithms, are available. For the study...

Romeo
 Referenced in 26 articles
[sw00812]
 modelchecking of reachability properties. It performs translations from TPNs to Timed Automata (TAs) that...

Concurrency Workbench
 Referenced in 12 articles
[sw14749]
 allows for various equivalence, preorder and model checking using a variety of different process semantics ... checking various semantic equivalences and preorders; define propositions in a powerful modal logic and check ... this logic; play Stirlingstyle modelchecking games to understand why a process does...

WebTLR
 Referenced in 8 articles
[sw09905]
 Modelchecking Web applications with WebTLR. WebTLR is a software tool designed ... modelchecking Web applications which is based on rewriting logic. Web applications are expressed ... using the Maude builtin LTLR modelchecker. WebTLR is equipped with a user ... navigation trace that underlies the failing model checking computation. This provides deep insight into...

Datalog LITE
 Referenced in 10 articles
[sw28894]
 deductive query language with linear time model checking. We present Datalog LITE, a new deductive ... query language with a lineartime modelchecking algorithm, that is, linear time data complexity...

Moby/DC
 Referenced in 5 articles
[sw01395]
 Moby/DC  A tool for modelchecking parametric realtime specifications. We define an operational subset ... tool MOBY/DC which implements a modelchecking algorithm for phase automata. The algorithm applies compositional ... modelchecking techniques and handles parameters by builtin procedures or by a link ... parameters the modelchecking problem is undecidable in general. Hence, we have to accept that...

HERMES
 Referenced in 9 articles
[sw00403]
 Most of protocol verification tools are modelchecking tools for bounded number of sessions, bounded...

KJava
 Referenced in 9 articles
[sw18991]
 Java. The semantics is applied to modelcheck multithreaded programs. Both the test suite...

CSHORe
 Referenced in 5 articles
[sw13319]
 verification techniques employing HORS modelchecking as their centrepiece. This paper contributes to the ongoing ... quest for a truly scalable modelchecker for HORS by offering a different, automata theoretic ... perspective. We introduce the first practical modelchecking algorithm that acts on a generalisation ... that prunes the CPDS prior to modelchecking and a method for extracting counterexamples...

REDLIB
 Referenced in 5 articles
[sw21175]
 technology of densetime system modelchecking in both academia and industry, we developed ... called REDLIB, which supports full TCTL modelchecking of densetime automata with multiple fairness...

Tac
 Referenced in 7 articles
[sw09455]
 single synchronous phase and many modelchecking queries can be captured using an asynchronous phase...

Helena
 Referenced in 6 articles
[sw33425]
 ModelChecking Helena Ensembles with Spin. The Helena approach allows to specify dynamically evolving ensembles...

Pinapa
 Referenced in 6 articles
[sw09955]
 analysis tools, ranging from ”superlint” to modelchecking. It is open source and available from...

MarCaSPiS
 Referenced in 5 articles
[sw06957]
 also have developed ways for modelchecking SoSL formulae against MarCaSPiS specifications by exploiting...