• ML

  • Referenced in 517 articles [sw01218]
  • requiring explicit type annotations, and ensures type safety – there is a formal proof that...
  • Kronos

  • Referenced in 273 articles [sw01270]
  • These systems are often part of complex safety-critical applications such as aircraft avionics, which...
  • CafeOBJ

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

  • Referenced in 170 articles [sw06888]
  • proof-carrying-code system, and a type safety proof for Standard...
  • Esterel

  • Referenced in 163 articles [sw20012]
  • tools that perform either bisimulation reduction or safety property checking. Esterel is now experimentally used...
  • Featherweight Java

  • Referenced in 91 articles [sw16204]
  • arguments about key properties such as type safety. We carry this process a step further ... following Java’s. A proof of type safety for Featherweight Java thus illustrates many ... interesting features of a safety proof for the full language, while remaining pleasingly compact ... give a detailed proof of type safety. The extended system formalizes for the first time...
  • BLAST

  • Referenced in 127 articles [sw02937]
  • function) by a valid execution. Verification of safety properties may be reduced to the reachability...
  • PHAVer

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

  • Referenced in 114 articles [sw13704]
  • with success to large embedded control-command safety critical real-time software generated automatically from...
  • seL4

  • Referenced in 84 articles [sw15222]
  • behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never...
  • CBMC

  • Referenced in 78 articles [sw09719]
  • allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and user-specified...
  • SLMC

  • Referenced in 71 articles [sw04604]
  • tool for verifying π-calculus systems against safety, liveness, and structural properties expressed...
  • SPARK

  • Referenced in 48 articles [sw03124]
  • absence of run-time errors in safety-critical software. This paper reports the results ... absence of run-time errors in safety-critical Ada software. In particular, the toolset...
  • VeriFast

  • Referenced in 57 articles [sw07705]
  • approach for the specification and verification of safety properties of pointer-manipulating imperative programs...
  • XDuce

  • Referenced in 54 articles [sw12436]
  • core, along with a proof of type safety...
  • d/dt

  • Referenced in 37 articles [sw10314]
  • describe the tool d/dt which provides automatic safety verification of hybrid systems with linear continuous ... continuous modes in order to satisfy a safety specification...
  • SIGNAL

  • Referenced in 51 articles [sw02915]
  • however made a difficult issue by global safety requirements. To enable separate compilation...
  • Ciao

  • Referenced in 47 articles [sw12088]
  • design objectives are high expressive power, extensibility, safety, reliability, and efficient execution...
  • MCNP

  • Referenced in 33 articles [sw07836]
  • within the United States by the Radiation Safety Information Computational Center in Oak Ridge ... radiation shielding, radiography, medical physics, nuclear criticality safety, detector design and analysis, nuclear oil well...
  • Uppaal2k

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