Universität UlmFakultät für Mathematik und WirtschaftswissenschaftenInstitut für Angewandte InformationsverarbeitungStatic Code Analysis inMulti-Threaded EnvironmentsDissertationzur Erlangung des Doktorgrades Dr. rer. nat. der Fakultät fürMathematik und Wirtschaftswissenschaften der Universität Ulmvorgelegt vonChristian Ehrhardtaus Mutlangen26. Oktober 2007AAmtierender Dekan: Prof. Dr. Frank StehlingGutachter: Prof. Dr. Franz SchweiggertProf. Dr. Helmut PartschProf. Dr.-Ing. Stefan JähnichenDr. Johannes MayerTag der Promotion: 26. Oktober 2007Who can understand his errors?Cleanse thou me from secret faults.Psalms 19.12, The BiblePrefaceThe notion that software might contain errors dates back to the famous annotationsof Lady Ada Lovelace to the description of the Analytical Engine designed by CharlesBabbage[36] where she states: “Granted that the actual mechanism [of the AnalyticEngine] is unerring in its processes, the cards may give it wrong orders. This isunquestionably the case; but there is much less chance of error, and likewise far lessexpenditure of time and labour, where operations only, and the distribution of theseoperations, have to be made out, than where explicit numerical results are to beattained.”Despite Lady Lovelace’s assessment, errors in software (i.e. today’s equivalent ofcards that give wrong orders) have become a predominant concern in software devel-opment and software engineering.