• CafeOBJ

  • Referenced in 171 articles [sw06232]
  • state transition systems. By capturing a set of states by a state predicate ... verify safety properties of infinite-state systems using predicate calculus in the set-theoretic iterative...
  • nuXmv

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

  • Referenced in 25 articles [sw04657]
  • used to model and verify infinite-state systems with variables of integer, Boolean, function...
  • Zapato

  • Referenced in 11 articles [sw25425]
  • produces abstract models of finite and infinite-state systems. When this process is applied...
  • Ivy

  • Referenced in 9 articles [sw41668]
  • liveness properties of parameterized and infinite-state systems via three modes: deductive verification using...
  • SLAB

  • Referenced in 8 articles [sw09875]
  • Certifying Model Checker for Infinite-State 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 infinite-state 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 infinite-state systems to the verification of complex embedded systems design ... compiled 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 ... network into an infinite-state transition system, which can be analyzed using SMT-based verification...
  • monabs

  • Referenced in 2 articles [sw18507]
  • state, system actions remain executable when new processes are added to the state. This concept ... well-established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate how monotonicity...
  • PICASSO

  • Referenced in 1 article [sw36776]
  • subsume a diverse range of infinite-state systems. Picasso computes an invariant of the input...
  • GBDD

  • Referenced in 1 article [sw15451]
  • framework for unified verification of infinite-state systems based on automata theory. It represents states...
  • InvA

  • Referenced in 2 articles [sw10124]
  • verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified...
  • INFAMY

  • Referenced in 5 articles [sw21177]
  • INFAMY: An Infinite-State Markov Model Checker. The design of complex concurrent systems often involves ... model checker for arbitrarily structured infinite-state 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 non-trivial (e.g. infinite-state) model checking algorithms to operate...
  • McScM

  • Referenced in 1 article [sw14482]
  • verification and controller synthesis of these infinite-state 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 SMT-based infinite-state 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...