• NuSMV

  • Referenced in 288 articles [sw04131]
  • based model checking component that includes an RBC-based Bounded Model Checker, which ... package use in the Bounded Model Checking algorithms...
  • HySAT

  • Referenced in 23 articles [sw01980]
  • HySAT: An efficient proof engine for bounded model checking of hybrid systems n this paper ... optimizations that arise naturally in the bounded model checking context, e.g. isomorphic replication of learned...
  • MCK

  • Referenced in 27 articles [sw09465]
  • algorithms, but MCK now also supports bounded model checking as well as explicit state model...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • verifier, for term-level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based...
  • LLBMC

  • Referenced in 15 articles [sw09478]
  • LLBMC: improved bounded model checking of C programs using LLVM . (Competition contribution). LLBMC ... programs. It is based on bounded model checking using an SMT solver and thus achieves ... LLBMC in contrast to other bounded model checking tools for C programs is that...
  • Pex

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

  • Referenced in 66 articles [sw04129]
  • models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features ... support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise ... bounded reachability analysis for continuous-time Markov decision processes (CTMDPs) and CSL model checking...
  • DiVer

  • Referenced in 10 articles [sw01938]
  • systems. We present a SAT-based model checking platform (DiVer) based on robust and scalable ... their respective roles are as follows: Bounded Model Checking (BMC) and Distributed BMC over...
  • FunFrog

  • Referenced in 6 articles [sw06571]
  • Funfrog: bounded model checking with interpolation-based function summarization. This paper presents FunFrog, a tool ... function summarization approach for software bounded model checking. It uses interpolation-based function summaries...
  • SAL

  • Referenced in 8 articles [sw13318]
  • model checker uses Yices to provide bounded model checking for systems defined over infinite data ... reals. In addition, both the bounded and infinite-bounded model checkers can prove invariants...
  • SATMC

  • Referenced in 8 articles [sw09469]
  • flexible platform for SAT-based bounded model checking [8] of security protocols. Under the standard ... strong typing, SATMC performs a bounded analysis of the problem by considering scenarios with ... general intruder based on the Dolev-Yao model...
  • PeRIPLO

  • Referenced in 7 articles [sw07896]
  • framework in two software bounded model checking applications: verification of a given source code incrementally...
  • Verics

  • Referenced in 6 articles [sw09464]
  • first one is based on Bounded Model Checking (BMC), while the second...
  • CPBPV

  • Referenced in 5 articles [sw00164]
  • which other frameworks based on bounded model checking have failed...
  • CalCS

  • Referenced in 5 articles [sw13098]
  • several benchmarks including formulas generated from bounded model checking of hybrid automata and static analysis...
  • CSP2SAT4J

  • Referenced in 4 articles [sw10081]
  • successful in recent years: Planning and Bounded Model Checking are two examples of applications...
  • CBMC

  • Referenced in 77 articles [sw09719]
  • CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports ... SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions ... specified as­ser­tions. Furthermore, it can check ANSI-C and C++ for consistency with...
  • HERMES

  • Referenced in 9 articles [sw00403]
  • protocol verification tools are model-checking tools for bounded number of sessions, bounded number...
  • Bedwyr

  • Referenced in 20 articles [sw09460]
  • sequent calculus can capture simple model checking problems as well as may and must behavior ... features allow reasoning directly on expressions containing bound variables...
  • FrankenBit

  • Referenced in 3 articles [sw25253]
  • Vectors, and bit-precise Bounded Model Checking, proving bit-precise safety, i.e. synthesizing a safe...