• JavaFAN

  • Referenced in 28 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 linear-time model-checking of finite-state systems. Being...
  • SatAbs

  • Referenced in 36 articles [sw12804]
  • ANSI-C. This paper presents a model checking tool, SatAbs, that implements a predicate abstraction ... using a SAT-solver. This allows the model checker to handle the semantics...
  • SMART_

  • Referenced in 33 articles [sw04097]
  • techniques, as well as symbolic CTL model-checking algorithms, are available. For the study ... process, but certain classes of non-Markov 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 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 ... check if a property specified in probabilistic computation tree logic (PCTL) [3] or continuous stochastic ... logic (CSL) is satisfied by a stochastic model. Furthermore, VESTA supports the statistical computation...
  • 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...
  • STeP

  • Referenced in 29 articles [sw17948]
  • finite-state systems, but combines model checking with deductive methods to allow the verification...
  • SPOT

  • Referenced in 20 articles [sw09473]
  • SPOT: an extensible model checking library using transition-based 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 transition-based 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 real-time 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]
  • model-checking 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...
  • PGSolver

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

  • Referenced in 14 articles [sw00562]
  • synthesis approach combining deep Model Checking and Genetic Programming. Given an LTL specification, genetic programming ... generating new candidate solutions, while deep model checking is used for calculating to what extent ... from the result of the deep model checking a fitness function that has a good...