• Bandera

  • Referenced in 133 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 69 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 31 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 37 articles [sw12913]
  • Smolka [LS98] for linear-time model-checking of finite-state systems. Being...
  • SMART_

  • Referenced in 33 articles [sw04097]
  • techniques, as well as symbolic CTL model-checking algorithms, are available. For the study...
  • Pex

  • Referenced in 32 articles [sw07263]
  • symbolic execution, similar to path-bounded model-checking) to determine test inputs for Parameterized Unit...
  • VESTA

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

  • Referenced in 25 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...
  • 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...
  • 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...
  • Datalog LITE

  • Referenced in 8 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...
  • 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...
  • K-Java

  • Referenced in 7 articles [sw18991]
  • Java. The semantics is applied to model-check multi-threaded programs. Both the test suite...
  • Tac

  • Referenced in 7 articles [sw09455]
  • single synchronous phase and many model-checking queries can be captured using an asynchronous phase...
  • 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...
  • FocusCheck

  • Referenced in 3 articles [sw01298]
  • programs We present the FocusCheck model-checking tool for the verification and easy debugging ... thereby enhancing usability and readability of model-checking results...