Presented at ESOP '09

Authors: Max Schäfer, Torbjörn Ekman, Oege de Moor

Abstract

Reference attribute grammars are a powerful formalism for concisely specifying and implementing static analyses. While they have proven their merit in practical applications, no attempt has sofar been made to rigorously verify correctness properties of the resulting systems. We present a general method for formalising reference attribute grammars in the theorem prover Coq. The formalisation is supported by tools for generating standard definitions from an abstract description and custom proof tactics to help automate verification.As a small but typical application, we show how closure analysis for the untyped lambda calculus can easily be implemented and proved correct with respect to an operational semantics. To evaluate the feasibility of our approach on larger systems, we implement name lookup for a naming core calculus of Java and give a formal correctness proof of the centerpiece of a rename refactoring for this language.

Accompanying technical report

Coq formalisation

BIBTEX:

 @inproceedings{esop09coq, 
           author = "Max Sch{\"a}fer and
                     Torbj{\"o}rn Ekman and
                     Oege de Moor",
           title = {{Formalising and Verifying Reference Attribute Grammars in Coq}}, 
           booktitle = "18th European Symposium on Programming (ESOP '09)", 
           editor = "Giuseppe Castagna", 
           year = "2009"}