
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 infinitestate 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 fixedpoint model checker OFMC for symbolic security protocol analysis, which extends ... demanddriven way, the transition system resulting from an IF specification. OFMC’s effectiveness ... integration of a number of symbolic, constraintbased 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 firstorder ... core of the system is a backward reachability procedure which symbolically computes preimages...

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 highperformance model checkers for LTL: symbolic, bounded, and infinitebounded. The infinitebounded ... 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 (BDDbased) 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 discretetime infinitestate 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 infinitestate transition ... system, which can be analyzed using SMTbased verification techniques (e.g. BMC, Kinduction...

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 toolsuite for the analysis and verification of systems ... specified as statetransition 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...