By: Simon Blanchoud and Yuanjian Wang Zufferey

Based on the paper of Patrick Cousot and Radhia Cousot

• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

Implemented in OCaml as we have in mind to get integrated into Jahob to be able to analyse real Java code.

Our goal is to compute the range of all variables in a piece of code as precisely as possible. These ranges could then be reused for latter analysis (e.g. possible division by 0, array out of bound, …).

• Fully analysis with one variable, loops, branches and sequences
• Use float values with operators +, -, * and /
• Uses both widening to ensure convergence and narrowing to precise the result

• Accept multiple variables
• Call to procedure

• Call to functions
• Arrays
• Object-oriented properties handling

• Our Report report_zufferey-blanchoud.pdf
• Our O'Caml Implementation variable_range-zufferey-blanchoud.tar
• Our class presentation presentation_zufferey-blanchoud.pdf