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



Tarski's Fixpoint Theorem

Continued in Lecture 07

sav10/lecture_06.txt · Last modified: 2010/04/12 12:06 by vkuncak