
NuSMV
 Referenced in 288 articles
[sw04131]
 based model checking component that includes an RBCbased 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 termlevel bounded model checking, correspondence checking, deductive verification, and predicate abstractionbased...

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 pathbounded modelchecking) 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 rewardbounded reachability probabilities, (propertydriven) bisimulation minimization, and precise ... bounded reachability analysis for continuoustime Markov decision processes (CTMDPs) and CSL model checking...

DiVer
 Referenced in 10 articles
[sw01938]
 systems. We present a SATbased 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 interpolationbased function summarization. This paper presents FunFrog, a tool ... function summarization approach for software bounded model checking. It uses interpolationbased 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 infinitebounded model checkers can prove invariants...

SATMC
 Referenced in 8 articles
[sw09469]
 flexible platform for SATbased 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 DolevYao 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 ANSIC and C++ programs. It also supports ... SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, exceptions ... specified assertions. Furthermore, it can check ANSIC and C++ for consistency with...

HERMES
 Referenced in 9 articles
[sw00403]
 protocol verification tools are modelchecking 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 bitprecise Bounded Model Checking, proving bitprecise safety, i.e. synthesizing a safe...