Transcript/Abstract Induction - Patrick Cousot
Transcript
Okay. And I think this is all I need to tell you about the logistics. So let's get started with the program itself. And it's my great pleasure to introduce Patrick Cousteau is our first speaker today. Patrick does not need much of an introduction. Everybody knows him and his work anyway. He got his PhD in 78 from the University of Grenada on Epstein interpretation, which he and his wife Radia invented, as we know, published a year before that in 77 and in 79. And he really changed the way we think about program analysis today, the way we do theory, the way we implement tools, the way we reason about program analysis. Much of that that's happening today is based on his work. And it's a great pleasure that he is here today to share some of his latest work in the area. I'm not going to give a long introduction. If I start enumerating his awards and prizes, we might not terminate before the coffee break. So I just hand over to Patrick and thanks for being here. So we have two plugs, we tried the other one, it works, it's not symmetric. So I'm going to speak on abstract induction. And to start with, I am going to speak about concrete induction, which is easier. And concrete induction is involved in any formal proof of a non trigger program, that is with looks and so on. And because program are proved by mathematical induction, that is by recurrence or something like that. So you have to invent an inductive argument, which is either an invariant or variant function or something like that. And this is the hardest part, because when you speak to mathematicians, they just give you the inductive argument. They never give you the proof. If you know the inductive argument, they think you are able to do the proof. Then to do the proof you have a base case, like entering the loop, and then an inductive case where you do one more iteration or something like that. And finally you prove that this inductive invariant argument is strong enough that this is imply the property that you want to prove. This is because in general, when you want to prove a property, it's not inductive. And like in math, when you prove a theorem, generally you have to prove a stronger fact than the theorem itself. So when you are confronted with this problem, the first thing computer scientists do is to avoid the problem so you can go unsound. This is not for scientists. I think you can do model checking. They should not be either for scientists because it's a bit trivial. There is no induction involved. You see, I follow the politically correct remark that's you then you have deductive methods that are quite popular also with theorem, provers, proof, verifiers, smt, solvers. There you avoid part of the problem because you ask the poor end user to provide inductive arguments. So he is doing all the work and then the machine is doing the trivial one. So it's still difficult to make the implication, but you are not responsible, it's the fault of the proverb, this is never your fault. Then there are guys that do finitary abstraction, I am one of these, but not very often. And that's completely equivalent to what is called predicate abstraction, which is just a reformulation of finite abstract domain. And it's also a bit trivial because you have only finitely many possible statement that can be inductive in the abstract domain. So you can check all of them. And this has a lot of limitations. And I will try to show you by an example. You see, if you take a program like X is zero, while X is less than some constant, and then I increment if I know the constant here I know the abstract domain that I can use to make the proof that at the end it's something like one in the loop, it's between zero and the bound. For each program there is a finite abstract domain that will allow me to make the proof. And so people conclude, because any abstract interpretation is finite, you can always do it with a finite domain. Yes, that's proof of one program. But when you take many program that is a programming language, then it's no longer the case because if you have a finite domain, you will miss some zero n. And for this zero n, you will not be able to make a proof of the program. Whereas if you take in trouble, they will do it without a problem. So this shows that if you have a finite domain only approach you can do for one program, but it doesn't scale to a programming language and to scale to a programming language there are infinite abstract domain that will always do better than you. So you will be always beaten by someone using an infinite domain. And it's because when you do induction, the inductive argument that you find in the infinite domain, there are many more than infinite domains, so your chances of success are much larger. So one other approach to avoid the difficulty of using infinite domains is refinement. That is, you take a finite domain, you fail for sure, you refine, you refill for sure and you go on like this until you get out of time or memory. So in that I would just explain a bit more formally. So in the case you have a Galway connection between a concrete domain of property that is a semantic domain, that is a property that is implication, this is the abstract domain, abstract implication and a galaxy connection between the two. What we do, we compute the abstraction of the collecting semantics, which is the strongest property of the semantics of the program. And sometimes we have an exact abstraction that is the abstraction of the collecting semantic, exactly, the abstract semantics. And sometimes we have another approximation because the abstraction loses information on this inductive argument. And so there is no way to have equality. But in both cases we are sound that says if some property over approximate the abstract semantics, you are sure that the semantics are this property. It might be possible that although you have the best approximation, yes, even if you have a best approximation here, or in that case it might be the case that you find some abstract argument, but it's inductive here. It shows it's inductive, but it does not imply the property that you want to prove. It's not strong enough. So the result on completeness is that it's always possible to refine the abstract domain I started with into another attract domain, which is more refinery, and so that I will have this commutation property which imply this equality, which imply that I can make the proof. So that's a result by Jacobezi, he will speak about it. And though this is really good news, that is, for any program, for one program, you will always be able to prove anything by abstract interpretation. The proof is a bit trivial, in fact, and it doesn't tell you how this is a problem in mathematics and mathematic machine. They never tell you how you approve their theorem, they just prove theorem. And you have to train yourself to do the theorem yourself. So that's the same problem in track interpretation. So now there are also bad news. And the bad news is that sometimes you have property where you have an intransic incompleteness. That is, the only refinement that I can do here is through identity. And so you have to go to the semantics to make the proof there is no way out. And so I will give you a very simple example. It's kind of model checking in a final space, but it's completely undecideable. And to do that, what I do, I consider an infinite future, which is the case in model checking, but also an infinite past. I got this idea over the Atlantic. I was thinking my plane is going to fly for five more minutes. So why? As I said, it's not because we departed from Paris, it's because the previous five minutes everything went okay. So the next five minutes everything will go okay. I don't have to start from the beginning. So even if my plane had been flying forever, then if it goes five minutes, good, next five would be good. Also maybe not ten, but ten. So you see the idea, you have a time origin, but you don't care. You have just a present time, the past and your future. And the operators are really classical. You can say something on the state, you can say something on the next transition that you are going to do, or the next state. And then the conjunction, the fixed point, and you have this operation which is reversal, which exchange the past and the future. So you take the previous picture you turn it around here, around I so you turn this. So you exchange past and future, so your logic can speak on the future. So now you have extended exchange, so it can also speak on the past. This operator allow you to speak both on past and future. And so now you can say something like in three minutes there will be something, because ten minutes before there was something that happened, and so half an hour later there will be something, because 1 hour before we had something. And so with this operation, although the space is finite, you can go to infinite things that can happen. So you are reasoning in a finite state of space, but the domain of property is in infinite domain. And so this is the source of incompleteness. If you want to do model check in, that is, you look for the traces that whenever you have an execution like this that goes through one such state, there will be a property of the future, which can be also of the past by just reversing. So if you want to do this instead of the for all you can do also the existOr path, then you have this abstraction that maps traces to places of sets. And the interesting point is that we prove that this abstraction is incomplete. We prove that in the original paper and then Jacob and prove a much more difficult result, which is any refinement of this abstraction will be incomplete, except if you go to the dentist, which is no abstraction at all. And so you see, even with finite state, so model checking is working not because it's finite state, it's because it's finite state and a very limited exclusivity of what you can prove. If you go to something more expressive, then even finite state are not enough. And you will always fail with any abstraction to prove everything in this language. So in practice, you get the situation. You see, I have represented here what is called the lattice of abstraction. That is, here you have identity, it's the most refined attraction. And here you have I don't know, you never know anything. That is, you always reply that all cases are possible. And in between this lattice, the points are program properties, like here some signs or some here you have inter. So what you do, you start with some abstraction here, say, and then you start refining. And if you are not lucky, you are going to refine forever. Because below you, you are in more and more precise domain, below you there is none which is inductive and strong enough. So you see, if I start from there, I have complete abstraction. It works here they are all incomplete. This one, this one is the only one which is complete here. And so this explain why refinement is a question of luck. See, if you are lucky at the beginning, you start with my stuff, or unlucky, you will get a result or none. So having a method based on luck is good if you believe in Probabilities for doing verification. So here is a little example, it's a filter. A filter is something that takes a signal and smooth it and here is a possible attraction which is here it takes its boxes or any convex will do when you make one loop iteration you see the invariant turns a little and shrink so you have a point outside. So if you want to remain in boxes you have to make a larger one and this will go forever. If you do refinement you will get this, you have a point outside and you see that the next point you will refine is one of these and it will go on forever until you cover the whole area here. So the only refinement that works is an ellipse. And to get this from a linear attraction to an ellipse, you have to understand this and then say yes, that's an ellipse and the nalibs will work. And you have to understand why it's because if you turn and shrink, it remains inside the ellipse, which is not completely trivial. This also will never terminate because you have to cover all points. And so if you don't go to an ellipse and stay to set of points or polydor or things like that, you will go on refining forever. So in general you need narrowing to stop this. So a trivial one is 20 minutes. And so Slam now is abandoned, which is pity, because in the original paper they claim that they were successful in 98% of the cases, which is always possible because you can just show the cases that were and so it takes 15 years to see that the 2% of the cases were the one you meet most often. So the only problem if that intelligence is needed for refinement and so this is still an open problem for some time. So now if you want to face the difficulty you have to do induction and in the abstract and that I will discuss now. So if you want to do sound software static analysis, you need some form of mathematical induction. It must be done in the abstract because it must be in some domain which is representable in a machine and mathematics are not in general. And it should be also said that if you apply in the abstract, it's valid in the concrete. So that the whole stuff that we have to discuss. There's an abstract domain that you consider to represent. The inductive argument should be infinite because we have seen be finite. When don't work, then the inductive argument must be strong enough to imply the property. So again, this encourage you to take complex rich abstract domain because you can express a lot but it must be inferrable in the abstract and then you want the simplest things possible because if the abstract domain is simple then it's easier to make inference. So there is a tension between expressivity and inferrability here which is the problem that we have to solve. I'm a very dry mouth. Yes, I have some water. Excuse me, I will take some water because I have very bad so it's opened does not explode when you it's a splash photo. So I will skip this slide because you spend too much time on it. No, it was just you have either two interpreters that reason on transitions or others like astray that reason on the structure of the program but in both cases you have the same problem. This doesn't solve any of the problem that we consider today. So in general you have some order the structure which can be a preorder, it's a bit more difficult. Then you have a transformer that simulate the effect of an induction step. And you want to compute a fixed point with goody protevis to have the fixed point which exists. And we are in this situation that I represent this way, you see, you have all points in D here. Then you have the points here for which F of X is less than X. Here you have the one where X is less than F of x. If you are in a positive here you have the fixed points and the classical method for finding the fixed point is to iterate from bottom. So you remain in this area until you reach the smallest of the fixed point here and you are done. The problem is that this will be infinite in general in an infinite domain. So the trick is the convergence criterion. When you reach something which is such that F of x is less than x, then you are sure to over approximate the least fixed point and this is coming from taski theorem or variants because there are many variants of the theorem. So the third thing is widening. So let's go to widenings. You have this increasing function that I have represented here. You have the iteration here and you see that it's converged slowly to the fixed point and we would like to accelerate this convergence. So what we can do here is instead of taking the function, we can take the tangent. If we take the tangent here, we will reach a point here which is such that F of x so you have x, f of x is larger than x and so you see F of x here is larger than x which is here and so you are sure to be above the fixed point. So the inventor of widening is Newton and this is not bad guy and it is reinvented recently by these people here and they call this Newton raption method for static analysis. The problem is that it's not always easy to define what is derivative or the tangent and when you go to narrowing, it's not trivial to find one because it doesn't guarantee that if you take a tangent, it does not guarantee that you are below the point where you started, but it's an idea. So just a little reminder, when you do extrapolation by widening, you start from bottom or something below the fixed point. Then either the next iterate is a positive point that is satisfied the convergence criterion and so you have found the result or it doesn't. And then you make an extrapolation of the previous iterate by the next one. And the widening is based on two independent epotes. The first one is you do an extrapolation, that is the result here will be larger than this one. And independently you can enforce convergence of increasing iterate with widening to the limit. So these two criteria are independent. And in my phobias, there were two chapters, one on widening, one on enforcing convergence. And many people say I have a widening, but it does not enforce conversion, so it's not widening. So it's not really true. Then the first widening, where this one you see, that's funny because at the time there was no text editor, so the bottom was a big square. And this one, this one is a later one where we had forgotten these two cases. To make it simpler, this one is interesting because it's coming a few years later. It has a threshold. That is when you do widening, if you go through zero, you stop at zero before widening to plus infinity. So when I go down, I go to zero or minus infinity. When I go up, I go to zero or plus infinity when I am larger. So this shows that you can always refine widening here by putting more and more threshold. And so whenever you give me widening, I will be able to give you a better one just by adding some thresholds like this. So there is no best widening. And so that's encouraging. You can publish forever by improving your widening. And this is discouraging because you will never make it. So the idea is this. You tap from bottom, you compute the next iterate and you pick these two elements, you widen and this give you something larger. You compute the next iterate from these two, you widen, this give you something larger until you reach something, so that the next iterate will be a positive point. That is when you go to apply the F to this point, it goes down. Okay? One problem with widening is that they are not increasing. And this is an example. You see, I have one one which is less than one two, and if I widen one one by one two, I get one plus infinity and it is not included. Shift here in one two wide down by one two, which is one two. So you see, this is smaller than that, this is the same and the result is larger here. So it proved that it's not increasing. And so in fact, it's not possible to have an increasing widening, because if you have a widening which is increasing its first parameter, which enforced termination of the generates and does not do over approximation, as soon as you have found a solution, that is, when you have a solution, the widening will not degrade the information. Then if you have these three cases, you cannot have these three properties simultaneously. So in practice we want to enforce the termination, we want to stop losing information when we have a solution, so it cannot be increasing in the first argument, obviously, if you take something like widening to top it's, increasing its first argument, it enforced termination, but it doesn't satisfy the last solution, so it's not good. So let's go to the narrowing, let's show the picture first. Maybe when we are going down, you can go on going down maybe forever and to slow down the progression to enforce the convergence, when you go down you can use a narrowing. So you start from the point that you have reached previously and then you narrow the previous iterate by the next one when you strictly decrease and you take the next iterate to be the solution, when the next iterate is a fixed point. And again, the narrowing has two independent importance. One is that you stay between the two values or the previous iterate and the next one, the way the narrowing is between these two values, so it's an interpolation and it enforced convergence of the decreasing iterate infinitely many steps. These two hypotheses are again independent and there are many widening narrowing that do not satisfy the second. For example, you just take the narrowing to be the argument F of y in general it is a narrowing by the definition, but it will not converge in general. So this was the first narrowing ever and if the previous iterate as an infinite bound, it takes one of the next iterate and otherwise it just takes the minimum of the two and it's the same for the upper bound, so it eliminates the infinite bound that have been introduced by the widening. It works like this, you see, you have an iterate, the previous one, you take something in between, you go on applying the f, you take something in between until you reach a fixed point. So now that you have reached a fixed point, you are blocked and de iterate. If you go on iterating, you are blocked here. So there is a notion of duality, which was in my thesis too, and which I made explicit in my thesis on widening because I thought it was not perfectly clear for people. And in the other chapter I said duality is a trivial notion. I will not go on typing two times. Same thing with the time. It took very long to retype the same thing. It's not now, you see, you just have a program to write the dual of your paper. You say. So the duality is this we have seen these two, the widening of the narrowing. So widening was for an increasing iteration, the narrowing was for decreasing iteration and the widening star from below it arrive above and the narrowing start above and arrive above the fixed point that you are looking for. So they are not dual. Now, if you take the dual, you have a dual narrative so it start above and arrive above. It start above and arrive below the fixed point and this one and the dual narrowing will dual narring will start below and arrive below. Okay? So you see that the widening, the extrapolators, they go outside two consecutive points and the dual narrowing and narrowing, they are interpolators, they go in between two successive points. So here are all the possible iteration. You see we have a widening, you have a fixed point, you start below and you arrive above. With the narrowing, we start above and rise above. And we were using the same point here PDC. And this is the dualum. You start above and you arrive below and you start below and you arrive below all these extrapolators, I use only two successive iterates. Obviously this is an option, you can also use three, four, five, any number and you can also make a widening on all previous iterates. And this is obviously more precise because you can't follow the evolution of the computation on a longer time. So the more you know about the computation, the more you can guess the future iterates. So examples are loop and rolling where you don't do widening at the first iteration in the loop, like in Astray or delayed widening, you do widening and then you make some iteration in the loop to cumulate information before doing one more extrapolation. So let's go to dual narrowing, dual narrowing, you start from below at the bottom you iterate. So this is one way of using the dual narrowing. What I do, I do a dual narrowing between the next iterate and the point where I stopped after the narrowing. So remember this point, this one here, I want to improve this, so I restart from bottom, but my iterate are guaranteed to remain below the point I have found. So I am sure that I will find something which is at least as good as the point where I arrived here and it may be that I find the same at the end, but it may also be that I find the most precise one. So the iterates are like this. I start from below, I take the next iterate and I do a dual narrowing with the point I want to stay below. And I do this when I have not a cos fixed point. That is, I have not reached the zone of stability. And when I have reached the zone of stability, then I delivered the last iterate, which I know was stable. So again, the dual laring has two independent input. It is one is when the next iterate. This is the previous iterate, that is the next iterate or that is the limit. Then I choose something in between it's an interpolation. I don't want to be aware that what I have found before. And the second is which is independent is that dual Narrang should enforce convergence of these iterates infinitely many steps. So here is an example of dual Narrating. You see, I have an interval here the next one. And I take something which is in the middle. You see, I take the middle of this and I take the middle of this. So if you imagine that this was the point I reached with the narrowing, you imagine that my infinity some number like in machine, like maximum or something like that, I can do this operation and I will try to improve by finding something in between. This was the first thing we try with Radiator to solve our equations. But we did not insist because finding the middle here is not really easy when you have nonumerical things. So we thought as nice for interval, it will not work for other things. That was a big error. So here the picture. You see, you take the next iterate. Then you have the point that we want to stay below and we take something in between here. I've taken the middle say. Then I reapply f and I take something in between two points here and we applyplay F. And at some point I have reached a fixed point, hopefully smaller than this one. In the worst case it will be the same as this one and I will have made no improvement. But in the best case I will have really improved this initial point. So I illustrate that with the case where you start with something that you have obtained by Wednesday and then narrowing. But it can also be used by Macmillan. It was used where this point is given by the specification of the user. And so you can do this iterate with knowing to improve the specification by the user to try to find something which is inductive and strong enough. My point doesn't need to be a fixed point here. I have never made the potential. That is why the fixed point can be anything even not comparable. Just to make the point peg interpolation you see, you are given P which is a logical formula which implies Q. So this is a previous iterate, this is a next iterate. And you are able to take interpolation to find something in between or next iterate rather user specification in the case of Magnificent and you find something in between with the additional property that the variable of the interpoland is included in the intersection of the variable of P and Q. But this hypertevis is just an extra hypotenuse. It's not needed in the correctness of the result. It was observed already by Dasilva and Aloe that it is narrowing. In fact, it's not. Narrowing, it's an inverse narrowing. We will see why next slide. But they had the idea and the problem is that I may not be unique. So you may have to try many to know which one works best or you have to be lucky, which is the same as trying many and it may not terminate. So you can say after two days of trial I will stop, declare that I cannot make it. So what is the relation between narrowing and dual narrowing? It's just the inverse. So it's a very strange property. You see, when you have a narrowing, it says this is a previous Italy, this is a previous Italian, this is the next one, it's decreasing and I find something in between with dual narrowing. This is my objective, I want to improve this, that is my next iterate and I pick something in between. And when you write it this way, you see that you just invert two parameters. And so if you know a narrowing, you will know dual narrowing either by just inverting. The problem is that the narrowing might be nice, inverted might not be so nice. That is, it might be something which is not adapted to what you want to do. But formally it is this relation. So another thing which is interesting is bounded widening and it's related to the things I have shown before. When you drink a little, it's very dry in the gut. Is it when you have a dual narrative, the thing you want to prove you have the next iterate and essentially you do a dual arrangement. There is a missing little ad which move there here. So the next iterate with the objective and you want it to be larger than the next Iterate to accelerate the iteration and more precise than the specification, not to overshoot the specification. So you do an induction on the next iterate and the specification bounded by the name. I think it was first used by Alvax for polydra, to force Polyedra to remain in two box. And the idea of this you have the previous iterate, the next iterate. You know that you would like to be in some box because for example, it's a machine integer. So you know, all machine integer must be in some box. And so what you do, you do bounded widening, which is like a widening, but we can ensure that the result will be smaller than b. So in that case, you have an induction on the previous iterate, the next iterate and the box. Whereas here you had only previous iterate and the box. And as I said before, when you do an induction on a larger past, you have better chance to be precise because the whole trick of widening is to extrapolate the previous behavior in the future. And the more knowledge you have of the previous behavior, the more chances you have to get the future right. This is well known in finance. They don't do that on one measure, they do that on extrapolation, on many, many, many measures, to be more precise. And so here is bounded by the name which is, you see, the previous iterate, the next iterate here, you have the box here. And what I do, I take the middle of the two, like I was doing before, and I retake the middle with the box. It just a suggestion so that this way of computing will take into account the previous two iterates. So if it's converged slowly, it will be more precise and if it converts fast, it will be less. If it converts slowly, yes, it will be fast. Excuse me, because I will have a little increment here, but I will have a large increment here. If it grows fast, I will have a large increment here and a smaller one here. So it compensates more or less the speed of convergence with the objective to try to find something that grows smoothly, in a sense. So that's it. When you have a dual lowering, you can always do a bounded widening and it can only be better. So it's time to finish now. What time is it? Yes, so I am finished almost. So one point is that you must be sound and recently I wrote a paper on which this presentation is built, where I try to have minimalist import evidence, that is where I say the minimum importer is to have the result I want to have on widening and things like that. So the third thing is that there is no need for lattices, partial orders and so on. So the only need is to have a concrete domain which is opposite. So in the concrete this is always true, because in math the fixed point equation for invariant, for example, are Postset, is only a concrete lattice and they have these fixed point which exists. Then the abstract domain can only be preordered and the concrete is the only thing you need. It doesn't need to be defined everywhere, it needs to be defined only for the iterate. Then the concrete transformer is increasing, but there is no need for any effort. There is on the abstract transformer in particular, when you have nested loop, the inner loop might contain widening, this will not be increasing, so the outer loop transformer will not be increasing. And so it's useless to have these emotiv sound increasing and the soundness of what EVs that I express in the abstract. If you express them in the concrete, you don't even need an order in the abstract just to make the comparison for stability, but elsewhere you don't need it. So this is independent of the termination property, which is another independent property. So, conclusion you will be happy. Challenge or verification is to infer an inductive argument and without deep knowledge about the program. That is, if you ask the user to tell you exactly what this program is doing, it's a bit cheating because real difficulty is finding this inductive argument from the program. Only the other thing which is difficult is to scale and to finish. I will give you my fabric example. This is a filter that is something that take a signal and smooth it. This is a simulation of the input. And my specification is that what is the interval or value of these two? S of zero and s of one? And if I add the user, they don't know because they are engineer, they have made the proof in the real world and they know in the real world and this is flow computation and they don't know and even they make errors. For example they take you see I have rounded because the numbers are secret. So this is not the real number that I have in the application, but the sum must be one if you make the sum and when they use real it is one, but then when they move to float there is a little error which is introduced and this creates an unstability and no one is aware of this. So one influence was that now they enter in exadesimal, the float in exadesimal to make sure the compiler will not make different choices depending on which compiler you have and they will do the rounding themselves so that the sum is one and this improved the result. So the challenge is this what is this number? And this is one possible number. And giving this to you is of no help because it's not inductive. And the induction is this little ellipse that we have seen. So you have to refine this interval into an ellipse to find the interval and this is the bulbs around the interval. This is a challenge of software verification. You have to say something that you don't know and in a way that is completely different from the things that are told to you that's it. So as like in tradition you have shown dual narrowing. This is old ideas and recently there was this instantiation with Craig interpolation and it can also be used as idea to improve fixed point when you are blood after widening, narrowing and at the end thank you, I am on time or not. So Patrick, as you know, there's a lot of work on composing program analyses and I'm wondering in this abstract induction, does it lend itself to composition as easily or are there some complications? If you want to compose inductive hypothesis, we have to be careful because if you do the most common composition is by the reduced product where you make the conjunction of separate analyzers. It might happen that you have a convergence in when it is domain. But when you do the reduced product, you lose the termination property. Because some domain is doing a widening. The other is saying wow, this is too large. I will make it smaller. It transfer the information to the domain that I've made the widening. We say I have improved and then it made the same widening and this goes forever. So you have to when you do the composition, you have to reprove the termination property. Not the soundness, the termination. Thank you. I had a question about this next to last slide. When you say no requirements or no hypothesis on the abstract transformers, what do you mean no requirements? Yeah. That is no increasing nest or mono TT you must say that they over approximate, but don't need to say they are increasing or monotonic or things like that, which is the importance that everybody does, which is forced with widening. Right, but you have to to say that you over approximate. If you take bottom, it doesn't work. So I was a bit oversimplifying, but in my head it's clear.
AUTO CHAPTERS
PATRICK COUSOT
Patrick Cousteau is our first speaker today. He really changed the way we think about program analysis today. Much of that that's happening today is based on his work. It's a great pleasure that he is here today to share some of his latest work.
CONCRETE INDUCTION VS. ABSTRACT INDUCTION
Concrete induction is involved in any formal proof of a non trigger program. In general, when you want to prove a property, it's not inductive. You will be always beaten by someone using an infinite domain. One other approach to avoid the difficulty of using infinite domains is refinement.
REFINEMENT IS A QUESTION OF LUCK
In between this lattice, the points are program properties. If you are not lucky, you are going to refine forever. Only refinement that works is an ellipse. Having a method based on luck is good if you believe in Probabilities for doing verification.
INCLINATION AND INFERRABILITY IN SOFTWARE STATIC ANALYSIS
If you want to do sound software static analysis, you need some form of mathematical induction. It must be done in the abstract because it must be in some domain which is representable in a machine. Third thing is widening. The inventor of widening is Newton.
DUALITY OF WIDERING AND NARROWING
So there is a notion of duality, which was in my thesis too. The more you know about the computation, the more you can guess the future iterates. Dual Narrang should enforce convergence of these iterates infinitely many steps.
BOUNDED WOUNDING AND DUAL ALGEBRA
B bounded widening is related to the things I have shown before. It was first used by Alvax for polydra, to force Polyedra to remain in two box. When you have a dual lowering, you can always do a bounded widening and it can only be better.
MINIMUM IMPORTANCE IN C#
There is no need for lattices, partial orders and so on. The only need is to have a concrete domain which is opposite. Challenge or verification is to infer an inductive argument from the program. Only the other thing which is difficult is to scale and to finish.
INTROSPECTION AND COMPOSITION
Patrick: Does abstract induction lend itself to composition as easily or are there some complications? If you want to compose inductive hypothesis, we have to be careful. Most common composition is by the reduced product. You have to reprove the termination property.
NO REQUIREMENT ON AXIAL TRANSFORMERS
When you say no requirements or no hypothesis on the abstract transformers, what do you mean no requirements? That is no increasing nest or mono TT you must say that they over approximate. So I was a bit oversimplifying, but in my head it's clear.