98 Pages
English
Gain access to the library to view online
Learn more

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

Gain access to the library to view online
Learn more
98 Pages
English

Description

TECHNISCHE UNIVERSITAT MUNCHENLehrstuhl fur Informatik 7Constraint Solving for Veri cationAshutosh Kumar GuptaVollst andiger Abdruck der von der Fakult at fur Informatik der Technischen Universit at Munc hen zurErlangung des akademischen Grades einesDoktors der Naturwissenschaften (Dr. rer. nat.)genehmigten Dissertation.Vorsitzender: Univ.-Prof. Dr. Helmut SeidlPrufer der Dissertation: 1. Univ.-Prof. Dr. Andrey Rybalchenko2. Full Prof. Dr. Rupak Majumdar,University of California/ USADie Dissertation wurde am 30.05.2011 bei der Technischen Universit at Munc hen eingereicht und durchdie Fakult at fur Informatik am 12.07.2011 angenommen.12AbstractSoftware is widely used and hard to make reliable. Researchers have been exploring new waysto ensure software reliability including software veri cation, i.e., mathematical reasoning aboutsoftware. The current technology for software veri cation is not su ciently e cient to be usedin industrial software production. In this thesis, we present novel constraint based veri cationmethods 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 thatimproves the e ciency of an important vd, namely template based invariantgeneration [16]. Then, we extend the template based invariant generation method to computebounds on consumption of a resource by a program.

Subjects

Informations

Published by
Published 01 January 2011
Reads 119
Language English

Exrait

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. Templates
are assertions over the program variables and parameters. By choosing values for the template parameters,
we select an assertion over program variables. Here, templates are used to represent the unknown invariants.
Using the program and a template, constraints are generated whose solutions are the invariants. The
generated constraints are non-linear, which are hard to solve.
Our algorithm is a heuristic approach that accelerates the non-linear constraint solving by taking advan-
tage of executions of the program. First, our algorithm collects test executions for the program. The program
states visited by the test executions must satisfy every correct instantiation of the invariant templates since
reachable states must satisfy the instantiation of the invariant templates. For each program state visited
by test executions, we replace program variables occurring in template by their values as determined by
the program state and obtain simpler constraints over template parameters. Then, we collect these linear
constraints for each visited program state. We conjoin these linear constraints with the original non-linear
9constraints and solve the result. The additional linear constraints are helpful in guiding a constraint solver
towards a solution of the non-linear constraints. As a result, the constraints are solved faster.
We designed and implemented a tool called InvGen that implements this heuristic and tested InvGen
on benchmarks. Results of the tests show that this heuristic is helpful for many examples. If the heuristic
fails to help then it does not slow down the overall solving either. We applied InvGen for computing ‘path
invariants’ [5] for counter examples in a CEGAR based tool Blast [45]. InvGen helps Blast to terminate
for some examples on which Blast did not terminate without InvGen.
Bound Synthesis: We extend template based invariant generation [16] to compute bounds on consumption
of a program resource, e.g., time, memory, or network bandwidth. We add an auxiliary variable and updates
on the variable to represent consumption of the resource. Together with an invariant template for each
program location, our bound synthesis method also assumes a template that expresses a space of linear
upper bounds over other program variables. Using these templates, we apply the algorithm of template
based invariant generation. A solution of the templates provides the symbolic expressions that bound the
consumption variable. We implemented this technique in a tool BoundGen.
C-to-Gates synthesis using BoundGen: We applied our bound synthesis algorithm for computing
bounds of heap consumption of C programs. We instantiated the resource as heap in the bound synthesis
algorithm. We combined BoundGen with a shape analysis tool Thor [63] and a hardware synthesis
toolchain. Using this combined toolchain, we directly synthesized hardware circuits from C programs that
allocate memory dynamically.
Part II : Constraint solving algorithms
In this part, 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 for solving recursion-free
Horn clauses over LI+UIF. We use these algorithms for re