• NuSMV

  • Referenced in 314 articles [sw04131]
  • NuSMV is a symbolic model checker developed as a joint project between: The Embedded Systems ... Information Technology at FBK-IRST The Model Checking group at Carnegie Mellon University , the Mechanized ... extension of SMV, the first model checker based on BDDs. NuSMV has been designed ... that includes an RBC-based Bounded Model Checker, which can be connected to the Minisat...
  • PRISM

  • Referenced in 454 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper we describe PRISM, a tool being developed ... probabilistic systems. PRISM supports three probabilistic models: discrete-time Markov chains, Markov decision processes...
  • Java PathFinder

  • Referenced in 123 articles [sw07658]
  • modeling language of the SPIN model checker. JPF translates a given JAVA program into ... PROMELA model. The PSIN model checker will then look for deadlocks and violations ... stated assertions. JPF generates a PROMELA model with the same state space characteristics ... previous work in applying existing model checkers and theorem provers to real applications...
  • Bandera

  • Referenced in 134 articles [sw07663]
  • property being checked. When a model-checker produces an error trail, Bandera renders the error...
  • MRMC

  • Referenced in 73 articles [sw04129]
  • outs of the probabilistic model checker MRMC. The Markov Reward Model Checker (MRMC...
  • Bebop

  • Referenced in 73 articles [sw08928]
  • Bebop: A Symbolic Model Checker for Boolean Programs. We present the design, implementation and empirical ... evaluation of Bebop—a symbolic model checker for boolean programs. Bebop represents control flow explicitly ... variable scoping, Bebop is able to model check boolean programs with several thousand lines...
  • CBMC

  • Referenced in 86 articles [sw09719]
  • CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports...
  • MCMAS

  • Referenced in 82 articles [sw09463]
  • MCMAS: A Model Checker for the Verification of Multi-Agent Systems. While temporal logic...
  • SLMC

  • Referenced in 74 articles [sw04604]
  • spatial logic specifications. The Spatial Logic Model Checker is a tool for verifying π-calculus ... logic for concurrency of Caires and Cardelli. Model-checking is one of the most widely...
  • ProB

  • Referenced in 71 articles [sw07084]
  • their specifications. ProB also contains a model checker and a refinement checker, both of which...
  • Uppaal2k

  • Referenced in 43 articles [sw01595]
  • visualize traces generated by the model-checker. Since version 3.4 the simulator can visualize ... verifier of Uppaal2k. A model-checker for automatic verification of safety and bonded-liveness properties...
  • MCK

  • Referenced in 33 articles [sw09465]
  • Model checking knowledge. MCK is a model checker for the logic of knowledge, developed ... testbed for a variety of approaches to model checking the logic ... knowledge. The novelty of this model checker is that it supports several different ways ... were based primarily on BDD-based model checking algorithms, but MCK now also supports bounded...
  • IF-2.0

  • Referenced in 46 articles [sw03303]
  • such as compilers, static analysers and model-checkers) as well as front-ends to various...
  • nuXmv

  • Referenced in 28 articles [sw18526]
  • nuXmv Symbolic Model Checker. This paper describes the nuXmv symbolic model checker for finite ... evolution of the nuXmv open source model checker. It builds on and extends nuXmv along ... Reals, and it provides advanced SMT-based model checking techniques. Besides extended functionalities, nuXmv...
  • OFMC

  • Referenced in 28 articles [sw09466]
  • open-source fixed-point model checker for symbolic analysis of security protocols. We introduce ... open-source fixed-point model checker OFMC for symbolic security protocol analysis, which extends ... model checker (the previous OFMC). The native input language of OFMC is the AVISPA Intermediate...
  • STP

  • Referenced in 44 articles [sw34795]
  • finders, cryptographic algorithms, intelligent fuzzers and model checkers. Features: Easy to embed or run standalone...
  • BEEM

  • Referenced in 30 articles [sw09815]
  • BEEM: Benchmarks for Explicit Model Checker. We present Beem — BEnchmarks for Explicit Model checkers. This...
  • SatAbs

  • Referenced in 41 articles [sw12804]
  • solver. This allows the model checker to handle the semantics of the ANSI-C standard...
  • Bogor

  • Referenced in 36 articles [sw06858]
  • Building your own software model checker using the Bogor extensible model checking framework Model checking...
  • WSAT

  • Referenced in 37 articles [sw01022]
  • manipulation are not supported by current model checkers...