• HyTech

  • Referenced in 309 articles [sw04125]
  • temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates...
  • PRISM

  • Referenced in 373 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 ... Markov chains. Analysis is performed through model checking such systems against specifications written ... tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs...
  • NuSMV

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

  • Referenced in 25 articles [sw11483]
  • Approximate probabilistic model checking. Symbolic model checking methods have been extended recently to the verification...
  • Cadence SMV

  • Referenced in 26 articles [sw07795]
  • Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal...
  • Quantor

  • Referenced in 22 articles [sw28381]
  • boolean formulas (QBF) in the QDIMACS format. Checking satisfiability of QBF, the QBF problem ... such as non-deterministic planning or symbolic model checking can be formulated succinctly...
  • SMART_

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

  • Referenced in 13 articles [sw04135]
  • system is a tool for checking finite state system against specifications in the temporal logic ... syntax. SMV uses the OBDD-based symbolic model checking algorithm to efficiently determine whether specifications...
  • Bebop

  • Referenced in 73 articles [sw08928]
  • empirical evaluation of Bebop—a symbolic model checker for boolean programs. Bebop represents control flow ... variable scoping, Bebop is able to model check boolean programs with several thousand lines...
  • visualSTATE

  • Referenced in 9 articles [sw07481]
  • significantly improve the efficiency of symbolic model checking of state/event models. It makes possible automated...
  • Spacer

  • Referenced in 7 articles [sw19496]
  • programs. We present an SMT-based symbolic model checking algorithm for safety verification of recursive...
  • UPPAAL TIGA

  • Referenced in 37 articles [sw12913]
  • algorithm we propose [CDFLL05] is a symbolic extension of the on-the-fly algorithm suggested ... time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm...
  • FIREMAN

  • Referenced in 6 articles [sw10594]
  • FIREMAN, a static analysis toolkit for firewall modeling and analysis. By treating firewall configurations ... programs, FIREMAN applies static analysis techniques to check misconfigurations, such as policy violations, inconsistencies ... among distributed firewalls. FIREMAN performs symbolic model checking of the firewall configurations for all possible...
  • Pex

  • Referenced in 32 articles [sw07263]
  • analysis (using dynamic symbolic execution, similar to path-bounded model-checking) to determine test inputs...
  • nuXmv

  • Referenced in 12 articles [sw18526]
  • Checker. This paper describes the nuXmv symbolic model checker for finite- and infinite-state synchronous ... evolution of the nuXmv open source model checker. It builds on and extends nuXmv along ... provides advanced SMT-based model checking techniques. Besides extended functionalities, nuXmv has been optimized...
  • PeRIPLO

  • Referenced in 6 articles [sw07896]
  • overapproximation to achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants...
  • JavaFAN

  • Referenced in 29 articles [sw01934]
  • Java program analysis framework, that can symbolically execute multithreaded programs, detect safety violations searching through ... finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses...
  • JPF-SE

  • Referenced in 10 articles [sw12038]
  • symbolic execution extension to Java pathfinder. We present JPF–SE, an extension ... Java PathFinder Model Checking framework (JPF) that enables the symbolic execution of Java programs...
  • Uppaal2k

  • Referenced in 42 articles [sw01595]
  • interface to the verifier of Uppaal2k. A model-checker for automatic verification of safety ... symbolic state-space. Since version 3.2 it can also check liveness properties. Generation of diagnostic...
  • p2b

  • Referenced in 2 articles [sw04983]
  • translation utility for linking Promela and symbolic model checking (tool paper) p2b is a research ... input syntax of the widely-used symbolic model checker SMV; it is then possible ... with SMV, as opposed to enumerative model checking with SPIN, the classical Promela verifier...