• Bandera

  • Referenced in 133 articles [sw07663]
  • Bandera tool set to model-check properties of concurrent Java software. The Bandera Tool ... model-checking Java source code. Bandera takes as input Java source code and a software ... specification language, and it generates a program model and specification in the input ... language of one of several existing model-checking tools (including Spin, dSpin...
  • ARMC

  • Referenced in 26 articles [sw04949]
  • ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. Software model checking with ... practical approach to verify industrial software systems. Its distinguishing characteristics ... tool, called ARMC (for Abstraction Refinement Model Checking), which has already been used for practical...
  • Zing

  • Referenced in 38 articles [sw01037]
  • Zing is a software model checking project at Microsoft Research. Our goal is to build ... scalable systematic state space exploration infrastructure for software. This infrastructure includes novel algorithms...
  • MOCHA

  • Referenced in 85 articles [sw12935]
  • MOCHA: Modularity in Model Checking. MOCHA is a growing interactive software environment for system specification...
  • Bogor

  • Referenced in 36 articles [sw06858]
  • Building your own software model checker using the Bogor extensible model checking framework Model checking ... software domains. We believe that recent trends in both the requirements for software systems ... systems are developed suggest that domain-specific model checking engines may be more effective than...
  • PIPER

  • Referenced in 28 articles [sw11478]
  • fundamental issues in making model checking viable for software. This paper proposes new techniques ... models as types, and (2) an assume-guarantee proof rule for carrying out compositional model ... checking on the types. Open simulation between CCS processes is used as both the subtyping...
  • nuXmv

  • Referenced in 12 articles [sw18526]
  • hybrid systems, safety assessment, and software model checking...
  • DAISY

  • Referenced in 32 articles [sw09059]
  • software tools have been proposed for automatically checking identifiability of nonlinear models. In this paper...
  • SLMC

  • Referenced in 69 articles [sw04604]
  • Cardelli. Model-checking is one of the most widely used techniques to check temporal properties ... software systems. However, when the analysis focuses on properties related to resource usage, localities, interference ... outperforms other tools for verifying systems modeled in π-calculus...
  • MRMC

  • Referenced in 66 articles [sw04129]
  • software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking...
  • SeaHorn

  • Referenced in 9 articles [sw18274]
  • state-of-the-art in software model checking and abstract interpretation for verification ... customizable framework for experimenting with new software verification techniques. The effectiveness and scalability of SeaHorn...
  • ASPIER

  • Referenced in 6 articles [sw09852]
  • ASPIER - the first framework that combines software model checking with a standard protocol security model ... iterative abstraction-refinement methodology for software model checking with a domain-specific protocol and symbolic...
  • StEAM

  • Referenced in 6 articles [sw01987]
  • model checker StEAM Most approaches for model checking software are based on the generation ... model checker for the verification of native c++-programs. To allow platform independent model checking...
  • SatAbs

  • Referenced in 36 articles [sw12804]
  • model checking tool, SatAbs, that implements a predicate abstraction refinement loop. Existing software verification tools ... using a SAT-solver. This allows the model checker to handle the semantics...
  • PeRIPLO

  • Referenced in 6 articles [sw07896]
  • producing effective interpolants in SAT-based software verification Propositional interpolation is widely used ... achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes ... framework in two software bounded model checking applications: verification of a given source code incrementally ... respect to various properties, and verification of software upgrades with respect to a fixed...
  • ACSAR

  • Referenced in 4 articles [sw02684]
  • ACSAR: Software model checking with transfinite refinement. ACSAR (Automatic Checker of Safety properties based ... Abstraction Refinement) is a software model checker for C programs in the spirit of Blast...
  • FunFrog

  • Referenced in 5 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 ... respect to state-of-the-art software model checkers...
  • McErlang

  • Referenced in 8 articles [sw09716]
  • McErlang is a software model checker for checking programs written in the Erlang programming language...
  • Web-TLR

  • Referenced in 8 articles [sw09905]
  • software tool designed for model-checking Web applications which is based on rewriting logic...
  • CBMC

  • Referenced in 71 articles [sw09719]
  • CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports ... specified as­ser­tions. Furthermore, it can check ANSI-C and C++ for consistency with ... procedure. While CBMC is aimed for embedded software, it also supports dynamic memory allocation using...