On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep
WG211/M14Blazy
From WG 2.11
Jump to navigationJump to search
Static analysis – the automatic determination of simple properties of a program – is the basis both for optimizing compilation and for verification of safety properties such as absence of run-time errors. To support the use of static analyses in verified compilers and in high-confidence verification environments, the analyses must be proved to be sound. In this talk, I will review some ongoing work in this direction in the CompCert and Verasco projects, in particular the construction and formal verification of a modular static analyzer based on abstract interpretation.
