Lab for Automated Reasoning and Analysis LARA

Lecture 06: Abstract Interpretation Background

Control-Flow Graphs and While Theorem: How to convert a program to have a single loop. What does this mean about invariants?

Loop invariant inference over a restricted set of invariants. Need for approximation.

Range Analysis Example

Partial Order

Partial Orders for Approximation

Lattices

Fixpoints

Tarski's Fixpoint Theorem

Continued in Lecture 07

 
sav10/lecture_06.txt · Last modified: 2010/04/12 12:06 by vkuncak
 
© EPFL 2018 - Legal notice