• Bandera

  • Referenced in 134 articles [sw07663]
  • Bandera tool set to model-check properties of concurrent Java software. The Bandera Tool ... components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input ... language of one of several existing model-checking tools (including Spin, dSpin ... customize the program model to the property being checked. When a model-checker produces...
  • SLMC

  • Referenced in 70 articles [sw04604]
  • spatial logic for concurrency of Caires and Cardelli. Model-checking is one of the most ... widely used techniques to check temporal properties of software systems. However, when the analysis focuses...
  • AGG

  • Referenced in 49 articles [sw04449]
  • graph parsing, consistency checking of graphs and conflict detection in concurrent transformations by critical pair ... include graph and rule-based modeling of software, validation of system properties by assigning...
  • Wolf

  • Referenced in 2 articles [sw01299]
  • concurrent C programs developed in IBM Haifa. It automatically generates both the model ... methods complement explicit exploration methods of software model checking...
  • Truth/SLC

  • Referenced in 8 articles [sw01623]
  • safety-critical concurrent systems where an ad hoc or conventional software engineering approach ... successful automated approach to verification, called model checking, in which one tries to prove that...
  • McErlang

  • Referenced in 7 articles [sw09716]
  • McErlang is a software model checker for checking programs written in the Erlang programming language ... standard Erlang runtime system that concerns distribution, concurrency and communication with a new runtime system...
  • SymmPa

  • Referenced in 3 articles [sw08414]
  • CEGAR) have enabled finite-state model checking of software written in mainstream programming languages. This ... applications of CEGAR to shared-variable concurrent software. We attribute this gap to the lack ... soundly overapproximates the original concurrent program. State explosion during model checking parallel instantiations of this...
  • CAESAR_SOLVE

  • Referenced in 14 articles [sw10194]
  • finite-state concurrent systems, such as equivalence checking and model checking. These problems ... this article, we present a generic software library dedicated to on-the-fly resolution...
  • CDSChecker

  • Referenced in 5 articles [sw21725]
  • CDSchecker: checking concurrent data structures written with C/C++ atomics. Writing low-level concurrent software ... level atomic operations and a weak memory model, enabling developers to write portable and efficient...
  • StEAM

  • Referenced in 6 articles [sw01987]
  • model checking software are based on the generation of abstract models from source code, which ... model checker for the verification of native c++-programs. To allow platform independent model checking ... object code for concurrent programs, we have extended an existing virtual machine...
  • Weak2SC

  • Referenced in 1 article [sw18521]
  • into account. This, however, makes most standard software verification tools inapplicable.{par}In this paper ... reducing the verification problem for weak memory models to the verification on SC. The reduction ... which can be fed into automatic model checking tools (like SPIN) as well as into ... example programs, ranging from concurrent data structures to software transactional memory algorithms...
  • monabs

  • Referenced in 2 articles [sw18507]
  • monotonicity in multi-threaded programs. Monotonicity in concurrent systems stipulates that, in any global state ... model checking can be at odds with monotonicity: predicate-abstracting monotone software can result ... result, pertinent well-established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate ... unbounded-thread model checker $mathsf{monabs}$ and applied it to numerous concurrent programs and algorithms...
  • CIVL

  • Referenced in 2 articles [sw34345]
  • creates a serious challenge for developers of software verification tools: it takes enormous effort ... typically targets one small part of the concurrency landscape, with little sharing of techniques ... CIVL: the Concurrency Intermediate Verification Language. CIVL provides a general concurrency model capable of representing ... back-end verifier which uses model checking and symbolic execution to check a number...
  • AdamMC

  • Referenced in 1 article [sw34180]
  • AdamMC can automatically encode concurrent updates of software-defined networks as Petri nets with transits ... reduction to a circuit model checking problem. We introduce a new reduction method that results...
  • EtomCRL2

  • Referenced in 1 article [sw22064]
  • reliable software system. Two approaches might be applied to model-check a system ... level. One is to directly apply model-checking algorithm to the programming language; the other ... investigated for model-checking the functional programming language Erlang. Correspondingly, two Erlang model-checkers McErlang ... model-checkers by applying them to verify a a distributed and concurrent example - telecoms implemented...
  • Gauss

  • Referenced in 2 articles [sw08835]
  • also employ shared memory threads to manage concurrency within smaller task sub-groups, capitalizing ... built a model extractor that extracts from MPI C programs a formal model consisting ... Microsoft’s Zing modeling language. MPI library functions are also being modeled in Zing. This ... avenues for problem- driven advances in software model-checking applied to scientific computing software development...
  • DTRON

  • Referenced in 0 articles [sw23642]
  • software requires methodologies and tools that address the problems of intrinsic concurrency and timing constraints ... paper we present DTRON, a framework for model-based testing that addresses the issues ... networked CPS. DTRON extends the Uppaal model checking tool and online test execution tool TRON...
  • Apron

  • Referenced in 66 articles [sw00045]
  • Apron: a library of numerical abstract domains for...
  • Coq

  • Referenced in 1764 articles [sw00161]
  • Coq is a formal proof management system. It...
  • GAP

  • Referenced in 2802 articles [sw00320]
  • GAP is a system for computational discrete algebra...