• CafeOBJ

  • Referenced in 171 articles [sw06232]
  • machine supported method for verifying safety properties of dynamic systems based on the first-order ... state predicate, we can verify safety properties of infinite-state systems using predicate calculus...
  • Esterel

  • Referenced in 165 articles [sw20012]
  • that perform either bisimulation reduction or safety property checking. Esterel is now experimentally used...
  • BLAST

  • Referenced in 129 articles [sw02937]
  • valid execution. Verification of safety properties may be reduced to the reachability, and BLAST...
  • PHAVer

  • Referenced in 117 articles [sw04123]
  • tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds...
  • seL4

  • Referenced in 90 articles [sw15222]
  • This encompasses traditional design and implementation safety properties such as the kernel will never crash...
  • VeriFast

  • Referenced in 64 articles [sw07705]
  • specification and verification of safety properties of pointer-manipulating imperative programs. The programmer may declare...
  • UPPAAL TIGA

  • Referenced in 45 articles [sw12913]
  • automata with respect to reachability and safety properties. Though timed games for long have been...
  • VerICS

  • Referenced in 35 articles [sw02011]
  • reachability analysis is available. For disproving safety properties, a new efficient method consisting in translating...
  • Featherweight Java

  • Referenced in 91 articles [sw16204]
  • enable rigorous arguments about key properties such as type safety. We carry this process...
  • TVLA

  • Referenced in 34 articles [sw09878]
  • doubly linked lists), to prove safety properties of Mobile Ambients, and to verify the partial...
  • SLMC

  • Referenced in 74 articles [sw04604]
  • verifying π-calculus systems against safety, liveness, and structural properties expressed in the spatial logic...
  • Mcmt

  • Referenced in 24 articles [sw11911]
  • deductive symbolic model checker for safety properties of infinite state systems whose state variables ... arrays. Theories specify the properties of the indexes and the elements of the arrays. Sets ... unsafe states and checks for safety and fix-points by solving Satisfiability Modulo Theories...
  • MOPS

  • Referenced in 23 articles [sw10117]
  • MOPS: an infrastructure for examining security properties of software. We describe a formal approach ... safe programming practice, encode them as safety properties, and verify whether these properties are obeyed...
  • LTSmin

  • Referenced in 21 articles [sw07214]
  • state space generation and verification of safety properties), reachability with symbolic state storage (vector...
  • Twelf

  • Referenced in 171 articles [sw06888]
  • language used to specify, implement, and prove properties of deductive systems such as programming languages ... proof-carrying-code system, and a type safety proof for Standard...
  • BEEM

  • Referenced in 30 articles [sw09815]
  • concrete instances) together with their correctness properties (both safety and liveness). The benchmark...
  • Cubicle

  • Referenced in 17 articles [sw13778]
  • model checker for verifying safety properties of parameterized systems. It implements a parallel symbolic backward...
  • Wolverine

  • Referenced in 13 articles [sw14483]
  • software verifier that checks safety properties of sequential ANSI-C and C++ programs, deploying Craig...
  • YASM

  • Referenced in 13 articles [sw09470]
  • their analysis towards proving that a (safety) property of interest holds (verification). On the other...
  • Uppaal2k

  • Referenced in 43 articles [sw01595]
  • checker for automatic verification of safety and bonded-liveness properties by reachability analysis...