The man of technology has learned to believe in justification, not by faith, but by verification!!!

Hi all...!! This is Farzana here and I hope you guys are enjoying the Summer School..😃 So well, here is a glimpse from Program Analysis and Verification (my all time favourite😍) lectured by Prof. K V Raghavan. He has been to our college a couple of months ago for 2 days lecture on the same topic. Today time didn't allow us for the complete lecture and with this post I will be adding some more elements that he taught us. So here we go.....👇

What is Program Verification?

Well...It is the algorithmic discovery of properties of a program by inspection of the source text. It is also known as static analysis, static program analysis, formal methods...

A verification approach: Abstract Interpretation!!

So here is the exact definition for abstract interpretation- A kind of program execution in which variables store abstract values from bounded domains, not concrete values.The program is executed on all abstract inputs and we observe the program properties from these runs.

Let's try an example!

Wanna try another example...?????????Solve....

So, that's all about abstract interpretation and hope you guys got a brief idea about it..😇 Now let's move on to the next topic.

Pointer Analysis!!!!

Let's begin with some definitions...

Points-to Analysis: Determine the set of possible values of a pointer-variable

Alias Analysis: Determine if two pointer-variables may point to the same location

What does it really mean when I say "p points to x"?????😕Well, it means “p stores the value &x” or “*p denotes the location x”. So let's try working out an example!

Example:

x = &a;                                    

y = &b;

if (?) {

p = &x;

} else {

p = &y;

}

*x = &c;--------------------------->x points to a..therefore a points to c

*p = &c;--------------------------->p points to x and y....therefore x points to a&c and y points to b&c

Solution:

x->a        y->b        p->x,y      a->null

x->a        y->b        p->x,y     a->c

x->a,c     y->b,c     p->x,y     a->c         

The above example will let us know about 2 related terms called:

Strong Update: a->c 

Weak Update :  x->a,c   and  y->b,c

(Try finding out why it is called so. Answers are welcomed on comment box😊)

Let's plow into some more analysis!! happy?????😃

Andersen's Analysis!!!

Let's have a look into this example:

1. x = &a;
2. *x = &w;
3. y = x;
4. x = &b;
5. *x = &t;
6. z = x;

So, how do you find solution for this? Here is the solution👇

In Andersen's analysis, initially all the variables will point to a null value. The table shows the variables pointing to at each statement. For example, at statement 1, x points to a,null while all other points to null initially.At statement 2, *x=&w means the variables where x is pointing-to points to w i.e,x is pointing to a,null and therefore a points to w. 

Steensgaard's Algorithm!!!

 We will try out finding solution for the same example above!

1. x = &a;
2. *x = &w;
3. y = x;
4. x = &b;
5. *x = &t;
6. z = x;

Solution..

The above solution is based on some rules👇

1. p=q

        Combine p's box and q's box.

2. p=&q

       Make p's box points to q's box. Whenever a box b points to 2 boxes b1 and b2,combine b1 and           b2.

3. p=*q

       Combine p's box with box pointed by q. Whenever a box b points to 2 boxes b1 and b2,combine         b1 and  b2.

4. *p=q

      Combine box pointed to by p with q's box.

Applications!!!💪

• Compiler Optimizations
• Verification and Bug finding

That's all about PAV...:)

Wishing you all great health and happiness!

God Bless!

With Regards,

Farzana Ishak

M.Tech Candidate

Government Engineering College Idukki, Kerala.