- Referenced in 134 articles
- 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...
- Referenced in 27 articles
- 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...
- Referenced in 38 articles
- 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...
- Referenced in 23 articles
- hybrid systems, safety assessment, and software model checking...
- Referenced in 91 articles
- MOCHA: Modularity in Model Checking. MOCHA is a growing interactive software environment for system specification...
- Referenced in 36 articles
- 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...
- Referenced in 45 articles
- software tools have been proposed for automatically checking identifiability of nonlinear models. In this paper...
- Referenced in 14 articles
- 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...
- Referenced in 28 articles
- 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...
- Referenced in 71 articles
- 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...
- Referenced in 70 articles
- software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking...
- Referenced in 6 articles
- 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...
- Referenced in 39 articles
- 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...
- Referenced in 6 articles
- 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...
- Referenced in 7 articles
- 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...
- Referenced in 6 articles
- 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...
- Referenced in 4 articles
- 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...
- Referenced in 92 articles
- logic programs. It combines the high-level modeling capacities of answer set programming (ASP) with ... checking (SAT). Unlike other learning ASP solvers, clasp does not rely on legacy software, such...
- Referenced in 78 articles
- CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports ... specified assertions. 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...
- Referenced in 30 articles
- Alloy is a lightweight language for software modelling. It’s designed to be flexible ... amenable to fully automatic simulation and checking. At its core, Alloy is a simple first...