Challenges and applications of assembly level software model checking [Elektronische Ressource] / von Tilman Mehler

ChallengesandApplicationsofAssembly LevelSoftwareModelCheckingDissertationzurErlangungdesGradeseinesDoktorsderNaturwissenschaftenanderUniversitätDortmundamFachbereichInformatikvonTilmanMehlerDortmund20052XXXXXXXXXXXXXXXXXXXXXTagdermündlichenPrüfung:Dekan/Dekanin: Prof. BernhardSteffenGutachter: Dr. StefanEdelkamp,Prof. KatharinaMorik.Note: ausgezeichnetsehrgutgutgenügendFürmeineEltern.4AcknowledgementsHereby, I would like to thank my advisor Dr. Stefan Edelkamp, for his excellent guid ance. Without his various original ideas, his broad theoretical and practical knowledge,his reviews and moral support, this thesis would not exist. Moreover, I thank Prof. Dr.Katharina Morik and Dr. Doris Schmedding who agreed to review my thesis. Also, Iwant to thank Shahid Jabbar for his support and his reviews. Further acknowledge ments must go to the German Research Society (DFG) who financially supported myresearch through the project Directed Model Checking with Exploration Algorithms ofArtificial Intelligence. Last, but not least, I would like to thank my girlfriend Frida aswellasmyfriendsandfamilyfortheirmoralsupport.56SummaryThis thesis addresses the application of a formal method called Model Checking to thedomain of software verification. Here, exploration algorithms are used to search forerrors in a program.