Abstract
The fifth seminar gave the floor to one of the pioneers of mechanized abstract interpretation, to deepen the simplified vision given in the fifth lecture. The speaker showed how to build an abstract interpreter " correct by construction " from a collecting semantics for the analyzed language and a compositional library of complete lattices. He then described the Verasco static analyzer, which is an abstract interpreter written and verified in Coq for the C# intermediate language of the CompCert verified C compiler, implementing complex abstract domains for memory states and for numbers.
