Constraint solving for verification [Elektronische Ressource] / Ashutosh Kumar Gupta. Gutachter: Andrey Rybalchenko ; Rupak Majumdar. Betreuer: Andrey Rybalchenko

Sujets

• Wissenschaft

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2011
• Nombre de lectures: 119
• Langue: English

Extrait

TECHNISCHE UNIVERSITAT MUNCHEN
Lehrstuhl fur Informatik 7
Constraint Solving for Veri cation
Ashutosh Kumar Gupta
Vollst andiger Abdruck der von der Fakult at fur Informatik der Technischen Universit at Munc hen zur
Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Helmut Seidl
Prufer der Dissertation: 1. Univ.-Prof. Dr. Andrey Rybalchenko
2. Full Prof. Dr. Rupak Majumdar,
University of California/ USA
Die Dissertation wurde am 30.05.2011 bei der Technischen Universit at Munc hen eingereicht und durch
die Fakult at fur Informatik am 12.07.2011 angenommen.
12Abstract
Software is widely used and hard to make reliable. Researchers have been exploring new ways
to ensure software reliability including software veri cation, i.e., mathematical reasoning about
software. The current technology for software veri cation is not su ciently e cient to be used
in industrial software production. In this thesis, we present novel constraint based veri cation
methods and algorithms for constraint solving that increase the e ciency of software veri cation.
In the direction of constraint based veri cation methods, we rst present an algorithm that
improves the e ciency of an important vd, namely template based invariant
generation [16]. Then, we extend the template based invariant generation method to compute
bounds on consumption of a resource by a program. In particular, we apply our bound compu-
tation algorithm on computing bounds of heap consumption of C programs.
In the direction of algorithms for constraint solving, we rst present a novel simplex
based proof production algorithm that is compatible with the simplex algorithm employed
in CLP(Q) [52]. Secondly, we present algorithm for solving recursion-free Horn clauses over
LI+UIF. We use these algorithms for re nement procedures in model-checkers to verify multi-
threaded programs, programs with procedures, and higher order functional programs.
34Acknowledgments
First and foremost, I am very grateful to my PhD supervisor Prof. Andrey Rybalchenko,
whose guidance was very productive for my development as a researcher. I also thank Prof.
Rupak Majumdar for reading this thesis and giving valuable comments.
I am thankful to Prof. Thomas Henzinger for teaching me course computer aided veri cation.
The course introduced me to the formal methods and veri cation. I found formal methods very
challenging and intellectually satisfying for their systematic view of computing. The encourage-
ment of Nir Piterman as a TA of the course also contributed in my nal decision to pursue PhD
in veri cation. I thank to the researchers with whom I collaborated for research work: Corneliu
Popeea, Ru-Gang Xu, Satnam Singh, Jiri Simsa, Viktor Vafeiadis, Byron Cook, and Stephan
Magill. Specially, I thank to Corneliu Popeea for working with me on a long running project. It
was wonderful experience to work with him.
I was a liated as a PhD student at EPFL, MPI-SWS, and TUMunich during the course of my
PhD. I enjoyed working at all the institutes and able to gather a wide experience of working at
di erent kinds of institutes in Europe. I would also like to thank my colleagues during my PhD:
Ruslan, Juan, Andreas, Jan, Atul, Animesh, Alan, Nuno, Mia, Max, Bimal, Malveeka, Pedro,
Surender, Simon, Dietmar, Maria, Barbara, and Vasu. They all made the institutes wonderful
places to be, and being in Europe is an experience that I will always treasure.
I would also like to thank my long term friends now living around the world: Prakash,
Mamta, Chaitanya, Manish, Vertika, Ajeeta, Vaibhav, Bramhdatt, Michael, Florance, Saad,
Adnan, Yogesh, and Sudhir. Occasional conversation with them always gives me a great joy.
I would like to thank my wife Divya. Her love and encouragement was vital for my success.
Finally, I would like to express my deep gratitude to my parents, my sister, and my brother-in-law
for their love and support during the ups and downs of graduate school. I am grateful beyond
words for all that they have given me.
56Contents
1 Introduction 9
2 Basic notation and programs 13
2.1 Basic notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Theory of linear arithmetic and uninterpreted functions . . . . . . . . . . . . . . . . . . . . . 13
2.3 Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
I Constraint based veri cation methods 15
3 From tests to proofs 17
3.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.2 Constraint-based invariant generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.3t simpli cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.4 Template-guided coverage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.5 InvGen: invariant generator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.6 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4 Bound synthesis 33
4.1 Resource bound analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5 C-to-gates synthesis using BoundGen 37
5.1 From heaps to arrays . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5.2 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5.3 Experimental results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
II Constraint solving algorithms 45
6 Introduction to interpolation 47
6.1 Interpolation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
6.2 Proof rules and proof trees forT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48LI+UIF
6.3 Algorithm for interpolation inT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
6.4 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
7 Proof producing CLP(LI+UIF) 53
7.1 CLP(Q) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
7.2 Cimmati et al.’s algorithm for proof production . . . . . . . . . . . . . . . . . . . . . . . . . . 62
7.3 Our algorithm for proof production . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
78 Solving recursion-free Horn clauses over LI+UIF 73
8.1 Recursion-free Horn clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
8.2 Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
8.3 Correctness and complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
8.4 Illustration: obtaining Horn clauses from re nement . . . . . . . . . . . . . . . . . . . . . . . 90
8.5 solving Horn clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
8Chapter 1
Introduction
Software is widely used. A personal computer may be executing millions of lines of source code to process the
complex interactions of di erent components of the computer. Designing reliable software is very hard due to
its high complexity and size. Currently, engineers in the software industry are applying many techniques to
increase the reliability of software, e.g., testing and code review. However, these techniques have limitations,
hence researchers have been exploring new ways to ensure software reliability. For example, mathematical
reasoning about software, which is known as software veri cation, has the potential to improve software
reliability. The methods for software veri cation are designed by composing the algorithms for constraint
solving as building blocks.
Current technology for software veri cation is not su ciently e cient to apply to large programs. In
this thesis, we will present novel constraint based veri cation methods and algorithms for constraint solving
that increase the e ciency of software veri cation. We only consider safety veri cation for programs that
are constructed using updates and condition expressions that are represented using conjunction of linear
(in)equalities. Along with this thesis, this class of programs has been focus of a large body of research
because many software applications are in this class and mathematical properties of the linear operations
leads to the development of veri cation methods with practical computation complexities.
Our contribution is separated in the two parts: constraint based veri cation methods and algorithms for
constraint solving.
Part I : Constraint based veri cation methods
In this part, we rst present an algorithm that improves the e ciency of an important veri cation method,
namely template based invariant generation [16]. Then, we extend the template based invariant generation
method to compute bounds on consumption of a resource by a program. In particular, we apply our bound
computation algorithm on computing bounds of heap consumption of C programs.
From tests to proofs: We rst present an algorithm that improves the e ciency of template based
invariant generation [16]. An invariant of a program is a super set of the reachable program states.