Abstraction refinement techniques for software model checking [Elektronische Ressource] / vorgelegt von Mohamed Nassim Seghir

Abstraction RefinementTechniquesfor Software Model CheckingDissertationzurErlangung des Doktorgradesder Technischen Fakult¨atder Albert-Ludwigs-Universit¨atFreiburg im Breisgauvorgelegt vonMohamed Nassim SeghirFreiburg im Breisgau2010Dekan: Prof. Dr. Bernd BeckerReferenten: Prof. Dr. Andreas PodelskiProf. Dr. Andrey RybalchenkoProf. Dr. Christoph SchollProf. Dr. Peter ThiemannDatum der Promotion: 16.12.2010AbstractSoftware model checking is a promising approach for the automatic verification ofsoftware systems. Many tools based on this approach have been implemented andsuccessfully applied to real world programs. Program abstraction is the key to theeffectivenessofsoftwaremodelchecking. Mostoftheexistingsoftwaremodelcheckersare based on the counterexample guided abstractionrefinement paradigm,commonlyknown as CEGAR, to efficiently abstract programs. Starting with a coarse abstrac-tion,theCEGARparadigmpermitstoiterativelyrefinethisabstractionuntilreachingan abstraction which is sufficiently precise to prove the property of interest. A prob-lemcommonto mostofthe existingtoolsis the divergenceofCEGARinthe presenceof loops. In particular, infinitely many (spurious) counterexamples may arise fromunfolding the same loop in a given program again and again. This problem is due tothe inefficiency of the abstraction refinement mechanisms used by these tools.