• Web-TLR

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

  • Referenced in 29 articles [sw01247]
  • 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...
  • AGG

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

  • Referenced in 3 articles [sw20979]
  • Eureka Tool for Software Model Checking. We describe EUREKA, a symbolic model checker for Linear...
  • jMocha

  • Referenced in 3 articles [sw24777]
  • automated debugging of embedded software. In model checking, a high-level description of a system ... model checker jMocha (Java MOdel-CHecking Algorithm) is based on this theme. Instead of manipulating ... hierarchical modeling framework of reactive modules. jMocha is a growing interactive software environment for specification ... verification both by symbolic and enumerative model checking; (4) implementation verification by checking trace containment...
  • ESBMC

  • Referenced in 7 articles [sw09946]
  • context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver ... verify single- and multi-threaded software (with shared variables and locks); (ii) to reason about ... properties using assert-statements, that are then checked as well. It also provides three approaches ... underapproximation and widening) to model check multi-threaded software. ESBMC can be invoked through...
  • Wolf

  • Referenced in 2 articles [sw01299]
  • methods complement explicit exploration methods of software model checking...
  • SIMP

  • Referenced in 2 articles [sw09936]
  • Specialization with constrained generalization for software model checking. We present a method for verifying properties ... operator and we address the problem of checking whether or not a safety property ... deriving, if possible, a program whose least model is a finite set of constrained facts ... with respect to state-of-the-art software model checkers...
  • 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 ... original concurrent program. State explosion during model checking parallel instantiations of this template...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • hardware and software systems. UCLID can be used to model and verify infinite-state systems ... verifier, for term-level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based ... date include microprocessor design verification, analyzing software for security exploits, and verifying distributed algorithms...
  • Gauss

  • Referenced in 2 articles [sw08835]
  • avenues for problem- driven advances in software model-checking applied to scientific computing software development...
  • TravMC

  • Referenced in 1 article [sw09396]
  • serve as a basis for software model checking for functional languages such...
  • EUFORIA

  • Referenced in 1 article [sw31587]
  • EUFORIA: complete software model checking with uninterpreted functions. We introduce and evaluate an algorithm ... style software model checker that operates entirely at the level of equality with uninterpreted functions...
  • DC2

  • Referenced in 1 article [sw15730]
  • scalable, scope-bounded software verification. Software model checking and static analysis have matured over ... last decade, enabling their use in automated software verification. However, lack of scalability makes these ... hard to apply. Furthermore, approximations in the models of program and environment lead...
  • JayHorn

  • Referenced in 1 article [sw25903]
  • JayHorn is a software model checking tool for Java. JayHorn tries to find a proof...
  • ObjectCheck

  • Referenced in 2 articles [sw00645]
  • Specifying software system designs with executable object-oriented modeling languages such as XUML, an executable ... verifying these system designs by model checking. However, state-of-the-art model checkers ... software system designs due to the semantic and syntactic gaps between executable object-oriented modeling ... supports an approach to model checking executable object-oriented software system designs modeled in xUML...
  • DeltaCCS

  • Referenced in 4 articles [sw14476]
  • Incremental model checking of delta-oriented software product lines. We propose DeltaCCS, a delta-oriented ... calculus CCS to formalize behavioral variability in software product line specifications in a modular ... propose a novel approach for incremental model checking of product lines. Therefore, variability-aware congruence...
  • SMART_

  • Referenced in 33 articles [sw04097]
  • describe the main features of Smart, a software package providing a seamless environment ... combine different formalisms in the same modeling study. For the analysis of logical behavior, both ... techniques, as well as symbolic CTL model-checking algorithms, are available. For the study...
  • MoCHi

  • Referenced in 9 articles [sw21478]
  • software model checker for a subset of OCaml. MoCHi is based on higher-order model ... checking, predicate abstraction, and CEGAR (see this paper for details...
  • Vensim

  • Referenced in 14 articles [sw12336]
  • Vensim is simulation software for improving the performance of real systems. Vensim is used ... dynamic feedback models. We emphasize: High quality, with dimensional consistency and Reality Checks™. Connections...