Results 1 to 20 of 499
Sort by:

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