• 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 71 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 42 articles [sw12913]
• Smolka [LS98] for linear-time model-checking of finite-state systems. Being...

• VESTA

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

• 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...

• C-SHORe

• Referenced in 5 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...

• 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...

• MarCaSPiS

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