- Referenced in 517 articles
- requiring explicit type annotations, and ensures type safety – there is a formal proof that...
- Referenced in 273 articles
- These systems are often part of complex safety-critical applications such as aircraft avionics, which...
- Referenced in 169 articles
- 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...
- Referenced in 170 articles
- proof-carrying-code system, and a type safety proof for Standard...
- Referenced in 163 articles
- tools that perform either bisimulation reduction or safety property checking. Esterel is now experimentally used...
- Referenced in 91 articles
- 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...
- Referenced in 127 articles
- function) by a valid execution. Verification of safety properties may be reduced to the reachability...
- Referenced in 116 articles
- tool for the exact veriﬁcation of safety properties of hybrid systems with piecewise constant bounds...
- Referenced in 114 articles
- with success to large embedded control-command safety critical real-time software generated automatically from...
- Referenced in 84 articles
- behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never...
- Referenced in 78 articles
- allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified...
- Referenced in 71 articles
- tool for verifying π-calculus systems against safety, liveness, and structural properties expressed...
- Referenced in 48 articles
- 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...
- Referenced in 57 articles
- approach for the specification and verification of safety properties of pointer-manipulating imperative programs...
- Referenced in 54 articles
- core, along with a proof of type safety...
- Referenced in 37 articles
- 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...
- Referenced in 51 articles
- however made a difficult issue by global safety requirements. To enable separate compilation...
- Referenced in 47 articles
- design objectives are high expressive power, extensibility, safety, reliability, and efficient execution...
- Referenced in 33 articles
- 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...
- Referenced in 43 articles
- model-checker for automatic verification of safety and bonded-liveness properties by reachability analysis...