• CafeOBJ

  • Referenced in 165 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 162 articles [sw20012]
  • that perform either bisimulation reduction or safety property checking. Esterel is now experimentally used...
  • BLAST

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

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

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

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

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

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

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

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

  • Referenced in 70 articles [sw04604]
  • verifying π-calculus systems against safety, liveness, and structural properties expressed in the spatial logic...
  • 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...
  • Twelf

  • Referenced in 169 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...
  • Mcmt

  • Referenced in 19 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...
  • BEEM

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

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

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

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

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

  • Referenced in 12 articles [sw04895]
  • system for a set of safety properties. However, unlike model checkers, ISP performs code level...