Formalising and Verifying Reference Attribute Grammars in Coq.
Reference attribute grammars are a powerful formalism for concisely specifying and implementing static analyses. While they have proven their meritin practical applications, no attempt has so far been made to rigorously verify correctness properties of the resulting systems. We present a general met...
| Egile Nagusiak: | , , |
|---|---|
| Beste egile batzuk: | |
| Formatua: | Conference item |
| Argitaratua: |
Springer
2009
|
| _version_ | 1826270948346560512 |
|---|---|
| author | Schäfer, M Ekman, T Moor, O |
| author2 | Castagna, G |
| author_facet | Castagna, G Schäfer, M Ekman, T Moor, O |
| author_sort | Schäfer, M |
| collection | OXFORD |
| description | Reference attribute grammars are a powerful formalism for concisely specifying and implementing static analyses. While they have proven their meritin practical applications, no attempt has so far been made to rigorously verify correctness properties of the resulting systems. We present a general method forformalising reference attribute grammars in the theorem prover Coq. The formalisationis 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 centre piece of a rename refactoring for this language. |
| first_indexed | 2024-03-06T21:48:56Z |
| format | Conference item |
| id | oxford-uuid:4a944b5e-6a1c-490c-a144-7f7737b34ebb |
| institution | University of Oxford |
| last_indexed | 2024-03-06T21:48:56Z |
| publishDate | 2009 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:4a944b5e-6a1c-490c-a144-7f7737b34ebb2022-03-26T15:38:19ZFormalising and Verifying Reference Attribute Grammars in Coq.Conference itemhttp://purl.org/coar/resource_type/c_5794uuid:4a944b5e-6a1c-490c-a144-7f7737b34ebbSymplectic Elements at OxfordSpringer2009Schäfer, MEkman, TMoor, OCastagna, GReference attribute grammars are a powerful formalism for concisely specifying and implementing static analyses. While they have proven their meritin practical applications, no attempt has so far been made to rigorously verify correctness properties of the resulting systems. We present a general method forformalising reference attribute grammars in the theorem prover Coq. The formalisationis 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 centre piece of a rename refactoring for this language. |
| spellingShingle | Schäfer, M Ekman, T Moor, O Formalising and Verifying Reference Attribute Grammars in Coq. |
| title | Formalising and Verifying Reference Attribute Grammars in Coq. |
| title_full | Formalising and Verifying Reference Attribute Grammars in Coq. |
| title_fullStr | Formalising and Verifying Reference Attribute Grammars in Coq. |
| title_full_unstemmed | Formalising and Verifying Reference Attribute Grammars in Coq. |
| title_short | Formalising and Verifying Reference Attribute Grammars in Coq. |
| title_sort | formalising and verifying reference attribute grammars in coq |
| work_keys_str_mv | AT schaferm formalisingandverifyingreferenceattributegrammarsincoq AT ekmant formalisingandverifyingreferenceattributegrammarsincoq AT mooro formalisingandverifyingreferenceattributegrammarsincoq |