• SMART_

  • Referenced in 33 articles [sw04097]
  • Logical and stochastic modeling with smart. We describe the main features of Smart, a software ... combine different formalisms in the same modeling study. For the analysis of logical behavior, both ... symbolic CTL model-checking algorithms, are available. For the study of stochastic and timing behavior...
  • VESTA

  • Referenced in 24 articles [sw08425]
  • model-checking VESTA uses a sequence of inter-related statistical hypothesis testing to check ... computation tree logic (PCTL) [3] or continuous stochastic logic (CSL) is satisfied by a stochastic...
  • MarCaSPiS

  • Referenced in 5 articles [sw06957]
  • Logic) has been introduced. This is a stochastic logic specifically designed for dealing with specific ... level, i.e. without having to change the model to investigate the effect of each assumption ... model-checking SoSL formulae against MarCaSPiS specifications by exploiting an existing state-based stochastic model...
  • prob-black-reach

  • Referenced in 2 articles [sw34625]
  • present a black-box checking technique for stochastic systems that allows both, non-deterministic ... involves model inference, testing and probabilistic model-checking. Here, we consider reachability checking...
  • GreatSPN

  • Referenced in 57 articles [sw00384]
  • GreatSPN2.0 is a software package for the modeling...
  • MiniSat

  • Referenced in 558 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • GLIM

  • Referenced in 189 articles [sw01126]
  • GLIM - a system for interactive fitting of generalized...
  • PRISM

  • Referenced in 434 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper...
  • Kronos

  • Referenced in 273 articles [sw01270]
  • KRONOS is a tool developed with the aim...
  • TAXYS

  • Referenced in 21 articles [sw01389]
  • TAXYS: A tool for the development and verification...
  • veriSoft

  • Referenced in 92 articles [sw01489]
  • VeriSoft automatically searches for coordination problems (deadlocks, etc...
  • MoDeST

  • Referenced in 32 articles [sw01544]
  • MoDeST --- a modelling and description language for stochastic...
  • BLAST

  • Referenced in 128 articles [sw02937]
  • BLAST (Berkeley Lazy Abstraction Software verification Tool) is...
  • LOTOS

  • Referenced in 152 articles [sw02961]
  • Introduction to the ISO specification language LOTOS. LOTOS...
  • SLAM

  • Referenced in 154 articles [sw03136]
  • SLAM is a project for checking that software...
  • TINA

  • Referenced in 45 articles [sw03280]
  • The tool TINA -- construction of abstract state spaces...
  • CPLEX

  • Referenced in 2676 articles [sw04082]
  • IBM® ILOG® CPLEX® offers C, C++, Java, .NET...
  • HyTech

  • Referenced in 330 articles [sw04125]
  • HyTech is an automatic tool for the analysis...
  • MRMC

  • Referenced in 70 articles [sw04129]
  • The ins and outs of the probabilistic model...