Wissing, KlausHerzog, OttheinRödiger, Karl-HeinzRonthaler, MarcKoschke, Rainer2019-05-152019-05-152007978-3-88579-206-1https://dl.gi.de/handle/20.500.12116/22493This 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.enText/Conference Paper1617-5468