• NuSMV

  • Referenced in 312 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 25 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 33 articles [sw09465]
  • algorithms, but MCK now also supports bounded model checking as well as explicit state model...
  • LLBMC

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

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

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

  • Referenced in 29 articles [sw09107]
  • FeynHiggs, ISASUGRA and SUSPECT. Accelerator bounds can be checked to identify viable dark matter candidates...
  • PolyTOIL

  • Referenced in 23 articles [sw14205]
  • checking of classes. The matching relation on types, which is related to F-bounded quantification ... both in stating type-checking rules and expressing the bounds on type parameters for polymorphism ... careful formal definition of type-checking rules and semantics. A proof of type safety...
  • CBMC

  • Referenced in 86 articles [sw09719]
  • 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...
  • 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 9 articles [sw13318]
  • model checker uses Yices to provide bounded model checking for systems defined over infinite data ... integers and reals. In addition, both the bounded and infinite-bounded model checkers can prove...
  • Ivy

  • Referenced in 9 articles [sw41668]
  • using an SMT solver, abstraction and model checking, and manual proofs using natural deduction ... compositional specification-based testing and bounded model checking. Ivy can extract executable distributed programs...
  • 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...
  • CalCS

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

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

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

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

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