- Referenced in 127 articles
- main function) by a valid execution. Verification of safety properties may be reduced...
- Referenced in 37 articles
- tool d/dt which provides automatic safety verification of hybrid systems with linear continuous dynamics with ... uncertain input. The verification procedure is based on a method for overapproximating reachable sets ... continuous modes in order to satisfy a safety specification...
- Referenced in 57 articles
- based approach for the specification and verification of safety properties of pointer-manipulating imperative programs ... datatypes and primitive recursive functions for specification. Verification proceeds by symbolic execution using an abstract...
- Referenced in 38 articles
- optimization, to solve, e.g., optimal control, safety verification, or estimation and fault detection problems...
- Referenced in 25 articles
- free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear ... abstraction is particularly useful for the safety verification problem which consists in checking whether...
- Referenced in 24 articles
- Safety verification of hybrid systems by constraint propagation based abstraction refinement This paper deals with ... problem of safety verification of non-linear hybrid systems. We start from a classical method...
- Referenced in 163 articles
- based verification tools that perform either bisimulation reduction or safety property checking. Esterel...
- Referenced in 167 articles
- behavioral system verification. We report on a machine supported method for verifying safety properties...
- Referenced in 43 articles
- Uppaal2k. A model-checker for automatic verification of safety and bonded-liveness properties by reachability ... properties. Generation of diagnostic traces in case verification of a particular real-time system fails...
- Referenced in 517 articles
- requiring explicit type annotations, and ensures type safety – there is a formal proof that ... compiler writing, automated theorem proving and formal verification. (wikipedia...
- Referenced in 18 articles
- state space generation and verification of safety properties), reachability with symbolic state storage (vector ... other hand, the implementation of a verification algorithm based on the PINS matrix automatically...
- Referenced in 11 articles
- based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular...
- Referenced in 14 articles
- Threader is a tool that automates verification of safety and termination properties for multi-threaded ... verified program. This paper describes the verification approach taken by Threader and provides instructions...
- Referenced in 77 articles
- allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified ... with other languages, such as Verilog. The verification is performed by unwinding the loops...
- Referenced in 7 articles
- Cousots (HMC), an algorithm that reduces verification of safety properties of typed higher-order functional ... logical refinement constraints whose satisfaction implies the safety of the source program. Next, it transforms ... abstract interpretation, HMC enables the fully automatic verification of programs written in modern programming languages...
- Referenced in 4 articles
- complies with the model so that offline verification results no longer apply, ModelPlex initiates provably ... guaranteed to imply that the offline safety verification results about the CPS model apply...
- Referenced in 6 articles
- that PKind significantly speeds up the verification of safety properties and, due to incremental invariant...
- Referenced in 4 articles
- ProMoVer: Modular verification of temporal safety properties This paper describes ProMoVer, a tool for fully ... verification of Java programs equipped with method-local and global assertions that specify safety properties ... natural instantiation of the modular verification paradigm, where correctness of global properties is relativized ... developed tool set for compositional verification of control flow safety properties, and provides appropriate...
- Referenced in 10 articles
- automatic program verification tool aimed at proving memory safety of C programs. It attempts...
- Referenced in 12 articles
- Yasm: A Software Model-Checker for Verification and Refutation. This paper presents Yasm ... towards proving that a (safety) property of interest holds (verification). On the other hand, since...