• FAST

  • Referenced in 38 articles [sw21268]
  • FAST: Fast Acceleration of Symbolic Transition Systems. fast is a tool for the analysis...
  • GeneSyst

  • Referenced in 5 articles [sw01303]
  • tool to build symbolic labelled transition systems from B specifications. The tool, called GeneSyst ... concrete hierarchical states. The resulting symbolic transition system represents all the behaviors of the initial...
  • nuXmv

  • Referenced in 26 articles [sw18526]
  • nuXmv symbolic model checker for finite- and infinite-state synchronous transition systems. nuXmv...
  • SMACS

  • Referenced in 2 articles [sw06144]
  • Symbolic supervisory control of infinite transition systems under partial observation using abstract interpretation. We propose ... state discrete event systems modelled by Symbolic Transition Systems. We provide models of safe memoryless...
  • OFMC

  • Referenced in 28 articles [sw09466]
  • source fixed-point model checker OFMC for symbolic security protocol analysis, which extends ... demand-driven way, the transition system resulting from an IF specification. OFMC’s effectiveness ... integration of a number of symbolic, constraint-based techniques, which are correct and terminating...
  • Mcmt

  • Referenced in 22 articles [sw11911]
  • deductive symbolic model checker for safety properties of infinite state systems whose state variables ... arrays. Sets of states and transitions of a system are described by quantified first-order ... core of the system is a backward reachability procedure which symbolically computes pre-images...
  • APMC

  • Referenced in 28 articles [sw11483]
  • Symbolic model checking methods have been extended recently to the verification of probabilistic systems. However ... representation of the transition matrix may be expensive for very large systems and may induce...
  • PESTS

  • Referenced in 2 articles [sw35864]
  • PESTS (Partial Evaluator of Symbolic Transition Systems) is a tool suite for the partial evaluation...
  • SIGREF

  • Referenced in 15 articles [sw00859]
  • implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures...
  • KORRIGAN

  • Referenced in 1 article [sw24328]
  • specification for mixed systems, i.e. systems with both dynamic (behaviour, communication, concurrency) and static (data ... notion behind a view is the symbolic transition system. A good environment supporting such...
  • SAL

  • Referenced in 9 articles [sw13318]
  • exploration and analysis of concurrent systems specified as transition relations. Its language includes many ... different high-performance model checkers for LTL: symbolic, bounded, and infinite-bounded. The infinite-bounded ... Yices to provide bounded model checking for systems defined over infinite data types, such...
  • mCRL

  • Referenced in 31 articles [sw29626]
  • micro CRL - written as mCRL if the symbol µ is not available) μCRL: A toolset ... verifying distributed systems in an algebraic fashion. It targets the specification of system behaviour ... LPOs. The instantiator generates a labelled transition system (LTS) from an LPO (under the condition...
  • LTSmin

  • Referenced in 18 articles [sw07214]
  • model checking and manipulating labelled transition systems. LTSmin already connects a sizeable number of existing ... safety properties), reachability with symbolic state storage (vector set), fully symbolic (BDD-based) reachability, distributed ... tools benefit from PINS2PINS optimizations, like local transition caching (which speeds up slow state space...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • verification of complex embedded systems design. HYDI extends the standard symbolic language SMV with timing ... into equivalent discrete-time infinite-state transition systems...
  • HyComp

  • Referenced in 4 articles [sw20163]
  • HyComp is a model checker for hybrid systems based on Satisfiability Modulo Theories (SMT). HyComp ... symbolic language. HyComp relies on the encoding of the network into an infinite-state transition ... system, which can be analyzed using SMT-based verification techniques (e.g. BMC, K-induction...
  • Ariel

  • Referenced in 2 articles [sw24050]
  • symbolic execution of hyperfinite ideal machines.par A hyperfinite ideal machine is a transition system...
  • Supremica

  • Referenced in 15 articles [sw18546]
  • systems is presented. The basic model in Supremica is finite automata where the transitions have ... data structure, a binary decision diagram, to symbolically represent the reachable states. Models in Supremica...
  • Z2sal

  • Referenced in 6 articles [sw07087]
  • Symbolic Analysis Laboratory (SAL) is a tool-suite for the analysis and verification of systems ... specified as state-transition systems. It allows different verification tools to be combined, all working...
  • TRANSIT

  • Referenced in 6 articles [sw28674]
  • TRANSIT: specifying protocols with concolic snippets. With the maturing of technology for model checking ... programming tools that can transform the way systems are specified. In this paper, we propose ... symbolic values. The proposed approach allows the programmer to describe the desired system partially using ... scenario corresponding to the counterexample. We describe TRANSIT, a language and prototype implementation...
  • ACTLW

  • Referenced in 7 articles [sw21031]
  • Action versus logics for transition systems, in: Semantics of Systems of Concurrent Processes, Proceedings LITP ... point characterisation of the operators together with symbolic algorithms for global model checking are shown...