Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars

Eric Van Wyk, Lijesh Krishnan

Research output: Contribution to journalArticlepeer-review

Abstract

Building verified compilers is difficult, especially when complex analyses such as type checking or data-flow analysis must be performed. Both the type checking and program optimization communities have developed methods for proving the correctness of these processes and developed tools for using, respectively, verified type systems and verified optimizations. However, it is difficult to use both of these analyses in a single declarative framework since these processes work on different program representations: type checking on abstract syntax trees and data-flow analysis-based optimization on control flow or program dependency graphs. We present an attribute grammar specification language that has been extended with constructs for specifying attribute-labelled control flow graphs and both CTL and LTL-FV formulas that specify data-flow analyses. These formulas are model-checked on these graphs to perform the specified analyses. Thus, verified type rules and verified data-flow analyses (verified either by hand or with automated proof tools) can both be transcribed into a single declarative framework based on attribute grammars to build a high-confidence language implementations. Also, the attribute grammar specification language is extensible so that it is relatively straight-forward to add new constructs for different temporal logics so that alternative logics and model checkers can be used to specify data-flow analyses in this framework.

Original languageEnglish (US)
Pages (from-to)109-122
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Volume176
Issue number3 SPEC. ISS.
DOIs
StatePublished - Jul 19 2007

Bibliographical note

Funding Information:
1 This research is partially funded by NSF CAREER Award #0347860, NSF CCF Award #0429640, and the McKnight Foundation. 2 Email: Van Wyk - evw@cs.umn.edu, Krishnan - krishnan@cs.umn.edu

Keywords

  • attribute grammars
  • compiler optimization
  • data flow analysis
  • model checking
  • optimization verification
  • temporal logic

Fingerprint Dive into the research topics of 'Using Verified Data-Flow Analysis-based Optimizations in Attribute Grammars'. Together they form a unique fingerprint.

Cite this