• ITS-Tools

  • Referenced in 2 articles [sw29142]
  • Symbolic Model-Checking Using ITS-Tools. We present verification toolset ITS-tools, featuring a symbolic...
  • p2b

  • Referenced in 2 articles [sw04983]
  • translation utility for linking Promela and symbolic model checking (tool paper) p2b is a research ... input syntax of the widely-used symbolic model checker SMV; it is then possible ... with SMV, as opposed to enumerative model checking with SPIN, the classical Promela verifier...
  • ACTLW

  • Referenced in 7 articles [sw21031]
  • operators together with symbolic algorithms for global model checking are shown. Usage of this...
  • PLSMC

  • Referenced in 1 article [sw14776]
  • symbolic model checker for propositional projection temporal logic. The formal specification languages for existing model ... PLSMC) is developed by implementing the symbolic model checking algorithm for PPTL from author ... previous work based on the acclaimed symbolic model checking system NuSMV. As PPTL ... system are checked with PLSMC. Experimental results show that the presented symbolic model checker...
  • FAST

  • Referenced in 37 articles [sw21268]
  • FAST: Fast Acceleration of Symbolic Transition Systems. fast is a tool for the analysis ... user must provide a model to analyse, the property to check and a computation policy...
  • PNMC

  • Referenced in 1 article [sw29139]
  • Model Checker for Petri Nets: pnmc. Symbolic model checking with decision diagrams is a very ... However, even when using advanced algorithms, model checking tools still need to be carefully written ... successful model checker and a failing one. We present pnmc, a symbolic model checker ... combination of advanced algorithms for symbolic model checking and advanced coding techniques offer very good...
  • STEWord

  • Referenced in 2 articles [sw20235]
  • theory and implementation. Symbolic trajectory evaluation (STE) is a model checking technique that has been ... register-transfer level descriptions, and how a model checker for the general theory ... including how word-level circuits can be symbolically simulated using a new encoding for words ... well as word-level bounded model checking...
  • Tempo

  • Referenced in 5 articles [sw11778]
  • automata. We present a symbolic on-the-fly model checking algorithm for event-recording automata ... forward reachability analysis and uses a symbolic representation of clock constraints. It forms the core ... suitable way and demonstrate that the model checking problem for this logic is decidable...
  • ASPIER

  • Referenced in 6 articles [sw09852]
  • methodology for software model checking with a domain-specific protocol and symbolic attacker model...
  • ENuSMV

  • Referenced in 1 article [sw13327]
  • been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is rather...
  • EUREKA

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

  • Referenced in 13 articles [sw20605]
  • checking trace equivalence of security protocols. It works in the so-called symbolic model, representing...
  • Mcmt

  • Referenced in 21 articles [sw11911]
  • mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite state ... which symbolically computes pre-images of the set of unsafe states and checks for safety ... heuristics for quantifier instantiation, specifically tailored to model checking, are at the very heart...
  • KRATOS

  • Referenced in 7 articles [sw07808]
  • capable of model checking the resulting C programs using the symbolic lazy predicate abstraction technique...
  • ConfigChecker

  • Referenced in 1 article [sw28842]
  • computation tree logic (CTL) and symbolic model checking to investigate all future and past states...
  • TASS_

  • Referenced in 3 articles [sw04889]
  • based parallel programs. TASS uses symbolic execution and model checking techniques to verify a number...
  • Sigma*

  • Referenced in 10 articles [sw21731]
  • represent inferred symbolic models, we use a variant of symbolic transducers that can be effectively ... composed and equivalence checked. Thus, Sigma* enables fully automatic analysis of behavioral properties such ... show experimentally. We also show how models inferred by Sigma* can boost performance of stream...
  • jMocha

  • Referenced in 3 articles [sw24777]
  • model checker jMocha (Java MOdel-CHecking Algorithm) is based on this theme. Instead of manipulating ... state-transition graphs, it supports the hierarchical modeling framework of reactive modules. jMocha ... requirements verification both by symbolic and enumerative model checking; (4) implementation verification by checking trace...
  • CIVL

  • Referenced in 2 articles [sw34345]
  • back-end verifier which uses model checking and symbolic execution to check a number...
  • HybridSal

  • Referenced in 7 articles [sw11781]
  • model checked by other SAL tools. HybridSAL has been used in Symbolic Systems Biology...