Static analysis of dynamic properties - automatic program verification to prove the absence of dynamic runtime errors
This paper introduces formal verification techniques applied by PolySpace Verifier as a static approach to measure dynamic software quality attributes. It is proving the correctness of atomic operations in the source code in regards to run-time errors. PolySpace is unique in assessing dynamic properties with a static analysis of the source code. The document outlines the use of the results during maintenance, re-engineering and also development of software. It also gives a short tool description and an overview about used methods and techniques, supported programming languages and requirements.
Full Text: PDF