UNIVERSITE PARIS DIDEROT–PARIS

Ahmed Bouajjani

Description

Niveau: Supérieur, Doctorat, Bac+8
UNIVERSITE PARIS DIDEROT–PARIS 7 ECOLE DOCTORALE DE SCIENCES MATHEMATIQUES DE PARIS CENTRE DOCTORAT INFORMATIQUE Cezara DRA˘GOI Automated verification of heap-manipulating programs with infinite data These dirigee par: Ahmed Bouajjani et Mihaela Sighireanu Soutenue le: 8 decembre 2011 Jury M. Ahmed Bouajjani co-directeur M. Roberto Di Cosmo president du jury M. Jean Goubault-Larrecq rapporteur M. Nicolas Halbwachs examinateur M. Viktor Kuncak examinateur M. Andreas Podelski rapporteur M. Shmuel Sagiv rapporteur Mme. Mihaela Sighireanu co-directrice

• specification des structures chaınees


• singly-linked lists


• verification des systemes logiciels


• decrivent des relations d'accessibilite entre les cellules de memoire


• reachability relations


• programmes avec memoire dynamique


• generation automatique de resumes

Sujets

• Marc Sangnier
• Shmuel
• Rousseau
• Maurice Halbwachs
• Roberto

Informations

• Publié par: profil-zyak-2012
• Publié le: 01 décembre 2011
• Nombre de lectures: 29
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

UNIVERSITE PARIS DIDEROT{PARIS 7
ECOLE DOCTORALE DE SCIENCES MATHEMATIQUES DE PARIS
CENTRE
DOCTORAT
INFORMATIQUE
Cezara DRAGOI
Automated veri cation of
heap-manipulating programs with
in nite data
These dirigee par: Ahmed Bouajjani et Mihaela Sighireanu
Soutenue le: 8 decembre 2011
Jury
M. Ahmed Bouajjani co-directeur
M. Roberto Di Cosmo president du jury
M. Jean Goubault-Larrecq rapporteur
M. Nicolas Halbwachs examinateur
M. Viktor Kuncak examinateur
M. Andreas Podelski rapporteur
M. Shmuel Sagiv rapporteur
Mme. Mihaela Sighireanu co-directrice2Abstract
In this thesis, we focus on the veri cation of safety properties for sequential programs
manipulating dynamic data structures carrying unbounded data. We develop a
logicbased framework where program speci cations are given by formulas. First, we address
the issue of automatizing pre/post-condition reasoning. We dene a logic, called CSL,
for the speci cation of linked structures or arrays, as well as compositions of these
structures. The formulas in CSL can describe reachability relations between cells in the heap
following some pointer elds, the size of the heap, and the scalar data. We prove that
the satis ability problem of CSL is decidable and that CSL is closed under the
computation of the strongest post-condition. Second, we address the issue of automatic synthesis
of assertions for programs with singly-linked lists. We de ne an abstract interpretation
based framework which combines a speci c nite-range abstraction on the shape of the
heap with an abstract domain on sequences of data. Di erent abstractions on sequences
are considered allowing to reason about their sizes, the multisets of their elements, or
relations on their data at di erent positions. We de ne an interprocedural analysis that
computes the e ect of each procedure in a local manner, by considering only the part
of the heap reachable from its actual parameters. We have implemented our techniques
in a tool which shows that our approach is powerful enough for automatic generation of
non-trivial procedure summaries and pre/post-condition reasoning.Resume
Le developpement de techniques rigoureuses et automatiques pour la veri cation des
systemes logiciels est une t^ache importante. Cette these porte sur la veri cation des
proprietes de suret^ e pour des programmes avec memoire dynamique et donnees in nies. Elle
developpe un cadre base sur la logique ou les speci cations des programmes sont donnees
par des formules. Premierement, nous considerons l’automatisation du raisonnement
pre/post-condition. Nous de nissons une logique, appelee CSL, pour la speci cation des
structures cha^ nees ou des tableaux, ainsi que des compositions de ces structures. Les
formules CSL decrivent des relations d’accessibilite entre les cellules de memoire, la taille
du tas et les donnees scalaires. Nous prouvons que le probleme de la satis abilite pour
CSL est decidable et que CSL est fermee par le calcul de la post-condition. Ensuite, nous
considerons la synthese automatique d’assertions pour des programmes avec des listes
simplement cha^ nees. Un cadre base sur l’interpretation abstraite est de ni qui
combine une abstraction nie sur la forme du tas avec une abstraction sur des sequences de
donnees. Les abstractions sur les sequences permettent de raisonner sur leurs tailles, les
multi-ensembles de leurs elements, ou les relations entre leurs donnees a des di erentes
positions. Nous denissons une analyse inter-procedurale qui calcule l’e et de chaque
procedure de fa con locale sur la partie du tas accessible a partir de ses parametres. Ces
techniques sont implantees dans un outil qui montre que notre approche est assez puissante
pour la generation automatique de resumes de procedure non-triviales et le raisonnement
pre/post-condition.
2Acknowledgements
First of all I would deeply like to thank my supervisors Mihaela SIGHIREANU and
Ahmed BOUAJJANI for their guidance and assistance during my phd. Together with
them I’ve walked on the solid ground of decidability and through the vast world of
abstractions. It was an enriching experience and a pleasure to work with you!
I would like to thank the reviews for their time and for their comments that helped
me improve this manuscript. Also, I would like to thank all the members of the jury for
accepting to participate to the defense of my phd thesis.
During my phd in LIAFA I was part of the Veri cation team where I met Tayssir
Touilli, Peter Habermehl, Eugene Asarin, Florian Horn and Arnaud Sangnier, amazing
people together with whom I’ve attended seminars, project meetings, and lunch breaks.
Noelle Degado and Nathalie Rousseau took care of all the administrative problems that
arose during my phd. I would like to thank them for their availability and e ciency.
I would like to thank all the phd students with whom I’ve shared, during these years,
an o ce, a co ee break or a Friday cake, and especially to the ones that were next by
me during the writing of this manuscript Adeline, Irene, Robin, Antoine, Denis, Herve,
Medhi, Luc, Thach, Stephane. Also, Claire, Marie, Mathilde, and Faouzi o ered me a
very warm welcome during my rst days in Paris and helped me accommodate to what
today is a familiar environment.
Along these years I have gained scienti c experience but also a few friends Linda,
Michael, and Roland. Our common interest in discovering Paris and its surroundings
brought me closer to them in the beginning. From there to daily activities and lots of
shared stories, it was just the logical sequence of facts. Despite the distance, my old
friends, Mihaela, Ionut , and Robert, stood really close to me during these years. To all
of them I would like to thank. Last but far from being the least, I would like to thank
Costin, with whom I’ve shared all the happy or sad, and funny or scary, moments of my
phd.
Finally, I would like to thank my parents Mihaela and Cezar for their patience, care,
and understanding. Also, I would like to thank my grandmother, to whom I dedicate this
manuscript.
34Contents
1 Introduction 9
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.1.1 Pre/post-condition reasoning . . . . . . . . . . . . . . . . . . . . . 11
1.1.2 Synthesis of program assertions . . . . . . . . . . . . . . . . . . . . 11
1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2.1 Pre/post-condition reasoning . . . . . . . . . . . . . . . . . . . . . 13
1.2.1.1 Logic gCSL . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.2.1.2 Logic CSL . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.2 Synthesis of program assertions . . . . . . . . . . . . . . . . . . . . 15
1.2.2.1 Abstract domains for programs manipulating singly-linked
lists over integers . . . . . . . . . . . . . . . . . . . . . . 16
1.2.2.2 Compositional inter-procedural analysis for programs
manipulating singly-linked lists over integers . . . . . . . . . 19
1.2.3 Celia: a tool for Static Analysis of C Programs with Dynamic Lists 24
1.3 Thesis organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2 Related work 27
2.1 Decidable logics for program veri cation . . . . . . . . . . . . . . . . . . . 27
2.2 Program analysis techniques . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3 Preliminaries 37
3.1 Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.2 Veri cation of transition systems . . . . . . . . . . . . . . . . . . . . . . . 39
3.3 Analysis of . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.3.1 Fixed point computations . . . . . . . . . . . . . . . . . . . . . . . 40
3.3.1.1 Fixed point approximations . . . . . . . . . . . . . . . . . 41
3.3.1.2 Chaotic iteration . . . . . . . . . . . . . . . . . . . . . . . 44
3.3.1.3 Combinations of abstract domains . . . . . . . . . . . . . 46
3.4 Numerical abstract domains . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4 Programs with dynamic data structures 51
4.1 Data types and program type system . . . . . . . . . . . . . . . . . . . . . 52
4.2 Programs without procedure calls . . . . . . . . . . . . . . . . . . . . . . . 54
4.2.1 Program syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.2.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
4.2.3 Program semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.2.3.1 Intra-procedural control ow graph . . . . . . . . . . . . 59
4.2.3.2 Representation of program con gurations . . . . . . . . . 60
4.2.3.3 Concrete transformers for program statements . . . . . . 63
4.2.3.4 Reachability collecting semantics . . . . . . . . . . . . . . 66
4.3 Extending programs with procedure calls . . . . . . . . . . . . . . . . . . 68
4.3.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.3.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
4.3.3 Program semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
5CONTENTS
4.3.3.1 Inter-procedural control ow graph . . . . . . . . . . . . 75
4.3.3.2 Representing relations between program con gurations . 77
4.3.3.3 Concrete transformers for program statements . . . . . . 78
4.3.3.4 for inter-procedural edges of the
ICFG . . . . . . . . .