Validation of data flow results for program modules [Elektronische Ressource] / vorgelegt von Karsten Klohs

Validation of Data Flow Results forProgram ModulesDissertationSchriftliche Arbeit zur Erlangung des akademischen Grades„Doktor der Naturwissenschaften“an der Fakultät für Elektrotechnik, Informatik und Mathematikder Universität Paderbornvorgelegt vonKarsten KlohsPaderborn, 2009Datum der mündlichen Prüfung:03.04.2009Gutachter:Prof. Dr. Uwe Kastens, Universität PaderbornProf. Dr. Jens Knoop, Technische Universität WienPromotionskommision:Prof. Dr. Uwe Kastens, Universität PaderbornProf. Dr. Jens Knoop, Technische Universität WienProf. Dr. Heike Wehrheim, Universität PaderbornProf. Dr. Heiko Platzner, Universität PnDr. Mathias Fischer, Universität PaderbornIIAbstractThis thesis presents a general approach to the validation of interprocedural dataflow results for separated software modules, in order to enable the safe use of dataflow results on devices which cannot aord to run the data flow analysis on theirown. The underlying idea stems from the “Proof-Carrying-Code Principle”[Nec97], which utilises that it is easier to check the correctness of a given solutionof a problem than to solve the problem.The requirement to validate analysis results originally arose for Java BytecodeVerification on Smart Cards.