• nuXmv

  • Referenced in 28 articles [sw18526]
  • provides advanced SMT-based model checking techniques. Besides extended functionalities, nuXmv has been optimized ... with requirements analysis, contract based design, model checking of hybrid systems, safety assessment, and software ... model checking...
  • ARMC

  • Referenced in 28 articles [sw04949]
  • ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. Software model checking with ... tool, called ARMC (for Abstraction Refinement Model Checking), which has already been used for practical...
  • UPPAAL TIGA

  • Referenced in 45 articles [sw12913]
  • Smolka [LS98] for linear-time model-checking of finite-state systems. Being...
  • JavaFAN

  • Referenced in 32 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...
  • Cadence SMV

  • Referenced in 27 articles [sw07795]
  • Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal ... verification is often equated with equivalence checking, model checking is substantially more general. It allows ... design process by building abstract system level models. Its use continues through the design refinement...
  • SatAbs

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

  • Referenced in 38 articles [sw01037]
  • Zing is a software model checking project at Microsoft Research. Our goal is to build...
  • SPOT

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

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

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

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

  • Referenced in 36 articles [sw14051]
  • decision procedures (validity as well as model checking) for temporal logics. In this paper...
  • 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 ... 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...
  • HySAT

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

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

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

  • Referenced in 28 articles [sw06956]
  • logic formula with a variety of model checking tools...
  • LIBRA

  • Referenced in 29 articles [sw10553]
  • Many graphical tools are provided for model checking and outlier detection. Most of the functions...
  • 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...