• NuSMV

• Referenced in 298 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 24 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 30 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 34 articles [sw07263]
• dynamic symbolic execution, similar to path-bounded model-checking) to determine test inputs for Parameterized...

• MRMC

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

• SAL

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

• 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...

• 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...

• CalCS

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

• 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...

• 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 21 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...