
CafeOBJ
 Referenced in 171 articles
[sw06232]
 state transition systems. By capturing a set of states by a state predicate ... verify safety properties of infinitestate systems using predicate calculus in the settheoretic iterative...

nuXmv
 Referenced in 28 articles
[sw18526]
 model checker for finite and infinitestate synchronous transition systems. nuXmv is the evolution ... finitestate systems it complements the basic verification techniques of nuXmv with state ... verification algorithms. For infinitestate systems, it extends the nuXmv language with new data types...

UCLID
 Referenced in 25 articles
[sw04657]
 used to model and verify infinitestate systems with variables of integer, Boolean, function...

Zapato
 Referenced in 11 articles
[sw25425]
 produces abstract models of finite and infinitestate systems. When this process is applied...

Ivy
 Referenced in 9 articles
[sw41668]
 liveness properties of parameterized and infinitestate systems via three modes: deductive verification using...

SLAB
 Referenced in 8 articles
[sw09875]
 Certifying Model Checker for InfiniteState Concurrent Systems. Systems and protocols combining concurrency and infinite ... state space occur quite often in practice, but are very difficult to verify ... automatically. At the same time, if the system is correct, it is desirable ... first certifying model checker for infinitestate concurrent systems. The tool uses a procedure that...

HyDI
 Referenced in 3 articles
[sw11912]
 Hybrid systems with Discrete Interaction. The purpose of the language is to apply state ... symbolic model checkers for infinitestate systems to the verification of complex embedded systems design ... compiled 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 ... network into an infinitestate transition system, which can be analyzed using SMTbased verification...

monabs
 Referenced in 2 articles
[sw18507]
 state, system actions remain executable when new processes are added to the state. This concept ... wellestablished safety checking algorithms for infinitestate systems become inapplicable. We demonstrate how monotonicity...

PICASSO
 Referenced in 1 article
[sw36776]
 subsume a diverse range of infinitestate systems. Picasso computes an invariant of the input...

GBDD
 Referenced in 1 article
[sw15451]
 framework for unified verification of infinitestate systems based on automata theory. It represents states...

InvA
 Referenced in 2 articles
[sw10124]
 verification of safety properties of infinitestate concurrent systems. Given a concurrent system specified...

INFAMY
 Referenced in 5 articles
[sw21177]
 INFAMY: An InfiniteState Markov Model Checker. The design of complex concurrent systems often involves ... model checker for arbitrarily structured infinitestate CTMCs. It checks probabilistic timing properties expressible...

IJIT
 Referenced in 1 article
[sw21506]
 programs. The API converts system states temporarily to program states just in time for expansion ... have effortlessly extended various nontrivial (e.g. infinitestate) model checking algorithms to operate...

McScM
 Referenced in 1 article
[sw14482]
 verification and controller synthesis of these infinitestate models. Our verification tool implements several model ... general framework for the class of transition systems with finite control/infinite data, McScM delivers...

JKind
 Referenced in 1 article
[sw21029]
 JKind is an SMTbased infinitestate model checker for safety properties in Lustre. JKind ... over time due to developments in both systems. Alternative Solvers (optional): By default, JKind...

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

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

TREX
 Referenced in 46 articles
[sw01388]
 TREX is a tool for automatic analysis of...

GreatSPN 1.7
 Referenced in 41 articles
[sw01562]
 GreatSPN 1.7: graphical editor and analyzer for timed...