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

Sujets

• Informatik

Informations

• Publié par: albert-ludwigs-universitat_freiburg
• Publié le: 01 janvier 2010
• Nombre de lectures: 7
• Langue: English

Extrait

Abstraction Refinement
Techniques
for Software Model Checking
Dissertation
zur
Erlangung des Doktorgrades
der Technischen Fakult¨at
der Albert-Ludwigs-Universit¨at
Freiburg im Breisgau
vorgelegt von
Mohamed Nassim Seghir
Freiburg im Breisgau
2010Dekan: Prof. Dr. Bernd Becker
Referenten: Prof. Dr. Andreas Podelski
Prof. Dr. Andrey Rybalchenko
Prof. Dr. Christoph Scholl
Prof. Dr. Peter Thiemann
Datum der Promotion: 16.12.2010Abstract
Software model checking is a promising approach for the automatic verification of
software systems. Many tools based on this approach have been implemented and
successfully applied to real world programs. Program abstraction is the key to the
effectivenessofsoftwaremodelchecking. Mostoftheexistingsoftwaremodelcheckers
are based on the counterexample guided abstractionrefinement paradigm,commonly
known as CEGAR, to efficiently abstract programs. Starting with a coarse abstrac-
tion,theCEGARparadigmpermitstoiterativelyrefinethisabstractionuntilreaching
an abstraction which is sufficiently precise to prove the property of interest. A prob-
lemcommonto mostofthe existingtoolsis the divergenceofCEGARinthe presence
of loops. In particular, infinitely many (spurious) counterexamples may arise from
unfolding the same loop in a given program again and again. This problem is due to
the inefficiency of the abstraction refinement mechanisms used by these tools.
TheaimofthisdissertationistheenhancementoftheCEGARprocessbytackling
the divergence problem from different sides. First, we introduce loop summaries, an
approach that goes beyond the abstraction of program states by abstracting transi-
tion relations induced by program loops over program states. Such an abstraction
permits to shortcut an infinite sequence of refinement steps. We provide experimen-
tal evidence showing how loop summaries boost the CEGAR process. Next, we treat
quantified assertions over arrays. Quantified assertions are used to express properties
over a (infinite) collection of array elements. We claim that careful adaptation of
existing software model checking techniques is sufficient to verify many interesting
properties over arrays. We support our claim by presenting a method for reasoning
about (unbounded) array segments. The underlying ingredients of our technique are
standardtomostsoftwaremodelcheckers. Thismakesourtechniqueeasilyintegrable
to other tools. Despite its simplicity our approach is surprisingly effective, it allowed
us to successfully verify quantified array assertions for both text book examples (se-
lection sort) and real-life examples taken from system code (e.g., device driver and
kernel code). Finally, we treat the modularity aspect regarding the verification of
quantified array assertions. We present a method based on assume guarantee rea-
soning to reduce the complexity of the verification task. The reduction affects the
code as well as the assertion to be verified. The implementation of this method con-
sists of a source-to-source transformation. The application of this technique did not
only improve performance of our tool but also enabled us to verify examples that are
challenging for automatic verification tools, such as insertion sort and bubble sort,
in addition to selection sort. To the best of our knowledge, there is only one work
in the literature proposing a method to handle these three sorting algorithms auto-
matically. We implemented ACSAR a software model checker for C programs. All
techniques presented in this thesis have been integrated into ACSAR. We provide an
experimental study for each technique.Kurzzusammenfassung
Software Model Checking ist ein vielversprechender Ansatz zur automatischen Ver-
ifikation von Software-Systemen. Auf der Grundlage dieses Ansatzes wurden viele
Werkzeuge implementiert und erfolgreich auf Programme aus der realen Welt ange-
wandt. Program Abstraktion ist der Schlu¨ssel zur Effektivita¨t von Software Model
Checking. Die meisten der bestehenden Software Model Checker basieren auf dem
Counterexample Guided Abstraction Refinement Paradigma, gemeinhin als CEGAR
bekannt, welches es erlaubt Programme effizient zu abstrahieren. Beginnend mit
einer groben Abstraktion, erlaubt das CEGAR Paradigma diese Abstraktion iterativ
zuverfeinern,bissiepr¨azisegenugist,umdieEigenschaftvonInteressenachzuweisen.
Ein Problem fu¨r die meisten auf CEGAR basierenden Werkzeuge ist die Divergenz
des Algorithmus in Anwesenheit von Schleifen. Insbesondere k¨onnen unendlich viele
(unechte)GegenbeispieleausderwiederholtenEntfaltungdergleicheSchleifeineinem
bestimmten Programm auftreten. Dieses Problem wird durch die Ineffizienz der Al-
gorithmen zur Verfeinerung der Abstraktion, die von diesen Werkzeugen verwendet
werden, verursacht.
Das Zielder vorliegendenDissertationist die Verbesserungdes CEGAR-Prozesses
durchLo¨sungdes Divergenz-ProblemsdurchverschiedeneAnsa¨tze. Zuerststellenwir
denAnsatzderLoopSummariesvor,dernichtwiebishernuru¨berProgrammzust¨ande
abstrahiert, sondern auch u¨ber Transitionsrelationen, die durch Schleifen u¨ber Pro-
grammzusta¨nde induziert werden. Dieser Ansatz erlaubt die Verku¨rzung einer un-
endlich langen Folge von Verfeinerungsschritten. Unsere Experimente belegen, dass
Loop Summaries den CEGAR-Prozess erheblich beschleunigen. Als na¨chstes behan-
deln wir quantifizierte Assertions u¨ber Arrays. Quantifizierte Aussertions werden
verwendet,umEigenschaftenu¨bereine(unendliche)SammlungvonArray-Elementen
auszudru¨cken. Wirbehaupten,dasseinesorgf¨altigeAnpassungdervorhandenenSoft-
ware Model Checking Techniken ausreichend ist, um viele interessante Eigenschaften
u¨ber Arrays zu u¨berpru¨fen. Wir stu¨tzen diese Behauptung auf ein von uns entwick-
eltes Verfahren zur Beweisfu¨hrung u¨ber (unbeschr¨ankte) Array-Segmente. Die zu-
grundeliegenden Bestandteile unserer Techniken sind Standard fu¨r die aktuelle Soft-
ware Model Checker. Dies erlaubt eine einfache Integration unserer Techniken in an-
dere Werkzeuge. Trotzseiner Einfachheit istunser Ansatz u¨berraschendwirksam: Er
erlaubt uns, quantifizierte Assertions u¨ber Arrays sowohl fu¨r akademische Beispiele
(z.B. Selection Sort) als auch fu¨r Beispiele aus realen Anwendungen (z.B. Treiber-
oder Kernel-Code)zu pru¨fen. Als Letztes behandeln wir den Aspekt der Modularit¨at
¨fu¨r die Uberpru¨fung von quantifizierten Assertions u¨ber Arrays. Wir pr¨asentieren
eine auf assume-guarantee-reasoningbasierende Methode zur Reduzierung der Kom-
plexita¨t der Verifikationsaufgabe. Die Reduktion beeinflusst sowohl den Code als
auch die zu u¨berpru¨fenden Assertions. Die Implementation dieser Methode erfolgt
als Code-zu-Code-Transformation. Die Implementierung dieser Technik verbesserte
nichtnurdieLeistungunseresWerkzeugssondernerlaubteunsauch,Beispielezuver-
ifizieren, die generell anspruchsvollfu¨r automatische Verifikationswerkzeuge sind, wie
z.B. Insertion Sort und Bubble Sort. Nach bestem Wissen gibt es in der bisherigen
Literatur nur einen Ansatz, der diese drei Sortieralgorithmen automatisch beweisen
kann. Um die in dieser Arbeit vorgestellten Techniken zu evaluieren, wurde AS-
CAR, ein Software Model Checker fr C Programme,in den diese Techniken integriert
wurden, implementiert. Die vorliegende Arbeit entha¨lt entsprechend experimentelle
Studien fu¨r jede der genannten Techniken.Acknowledgments
I would like to express my sincere gratitude to all of you
who directly or indirectly supported me in a number of ways.
This thesis would have never been possible without you.To my family.Contents
1 Introduction 1
1.1 Software Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Predicate Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.3 CEGAR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.4 Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.5 Thesis Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2 Preliminaries 5
2.1 Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.2 Symbolic State Representation . . . . . . . . . . . . . . . . . . . . . . 7
2.3 Symbolic Transformers . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.3.1 Forward Transformer Post . . . . . . . . . . . . . . . . . . . . . 7
2.3.2 Backward Transformer Pre . . . . . . . . . . . . . . . . . . . . 7
2.4 Trace. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.5 Model Checking Problem . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.6 Verifying Safety Properties . . . . . . . . . . . . . . . . . . . . . . . . 8
2.7 Invariant Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.8 Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.9 Predicate Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.9.1 Lattice of Symbolic States . . . . . . . . . . . . . . . . . . . . . 10
2.9.2 Abstract Transformer . . . . . . . . . . . . . . . . . . . . . . . 10
2.10 Counterexample Guided Abstraction Refinement (CEGAR) . . . . . . 11
3 Backward State Exploration 13
3.1 The Backward Search Algorithm . . . . . . . . . . . .