-
Bandera
- Referenced in 134 articles
[sw07663]
- Using the Bandera tool set to model-check properties of concurrent Java software. The Bandera ... components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input ... language of one of several existing model-checking tools (including Spin, dSpin ... model to the property being checked. When a model-checker produces an error trail, Bandera...
-
SLMC
- Referenced in 74 articles
[sw04604]
- model checking concurrent systems against dynamical spatial logic specifications. The Spatial Logic Model Checker ... concurrency of Caires and Cardelli. Model-checking is one of the most widely used techniques...
-
CMC
- Referenced in 34 articles
[sw12422]
- Tool for Compositional Model-Checking of Real-Time Systems. In this paper we present ... tool (CMC) for compositional model-checking of real-time systems. CMC is based...
-
UPPAAL TIGA
- Referenced in 45 articles
[sw12913]
- Smolka [LS98] for linear-time model-checking of finite-state systems. Being...
-
VESTA
- Referenced in 25 articles
[sw08425]
- probabilistic systems. It supports statistical model-checking [6, 7] and statistical evaluation of expected values ... temporal expressions. For model-checking VESTA uses a sequence of inter-related statistical hypothesis testing...
-
Pex
- Referenced in 35 articles
[sw07263]
- symbolic execution, similar to path-bounded model-checking) to determine test inputs for Parameterized Unit...
-
SMART_
- Referenced in 33 articles
[sw04097]
- techniques, as well as symbolic CTL model-checking algorithms, are available. For the study...
-
Romeo
- Referenced in 26 articles
[sw00812]
- model-checking 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 Stirling-style model-checking games to understand why a process does...
-
Web-TLR
- Referenced in 8 articles
[sw09905]
- Model-checking Web applications with Web-TLR. Web-TLR is a software tool designed ... model-checking Web applications which is based on rewriting logic. Web applications are expressed ... using the Maude built-in LTLR model-checker. Web-TLR 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 linear-time model-checking algorithm, that is, linear time data complexity...
-
C-SHORe
- Referenced in 6 articles
[sw13319]
- verification techniques employing HORS model-checking as their centrepiece. This paper contributes to the ongoing ... quest for a truly scalable model-checker for HORS by offering a different, automata theoretic ... perspective. We introduce the first practical model-checking algorithm that acts on a generalisation ... that prunes the CPDS prior to model-checking and a method for extracting counter-examples...
-
Moby/DC
- Referenced in 5 articles
[sw01395]
- Moby/DC -- A tool for model-checking parametric real-time specifications. We define an operational subset ... tool MOBY/DC which implements a model-checking algorithm for phase automata. The algorithm applies compositional ... model-checking techniques and handles parameters by built-in procedures or by a link ... parameters the model-checking problem is undecidable in general. Hence, we have to accept that...
-
HERMES
- Referenced in 9 articles
[sw00403]
- Most of protocol verification tools are model-checking tools for bounded number of sessions, bounded...
-
K-Java
- Referenced in 9 articles
[sw18991]
- Java. The semantics is applied to model-check multi-threaded programs. Both the test suite...
-
REDLIB
- Referenced in 5 articles
[sw21175]
- technology of dense-time system model-checking in both academia and industry, we developed ... called REDLIB, which supports full TCTL model-checking of dense-time automata with multiple fairness...
-
Tac
- Referenced in 7 articles
[sw09455]
- single synchronous phase and many model-checking queries can be captured using an asynchronous phase...
-
Helena
- Referenced in 6 articles
[sw33425]
- Model-Checking 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 model-checking. It is open source and available from...
-
ITS-Tools
- Referenced in 3 articles
[sw29142]
- Symbolic Model-Checking Using ITS-Tools. We present verification toolset ITS-tools, featuring a symbolic ... model-checking back-end engine based on hierarchical set decision diagrams (SDD) that supports reachability ... model-checking and a user-friendly eclipse based front-end. Using model transformations...