Loading...
Please wait, while we are loading the content...
Similar Documents
Using verified data-flow analysis-based optimizations in attribute grammars (2006)
| Content Provider | CiteSeerX |
|---|---|
| Author | Wyk, Eric Van Krishnan, Lijesh |
| Description | 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 modelchecked 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. Key words: compiler optimization, optimization verification, data flow analysis, attribute grammars 1 |
| File Format | |
| Language | English |
| Publisher Date | 2006-01-01 |
| Publisher Institution | In Proc. Intl. Workshop on Compiler Optimization Meets Compiler Verification (COCV |
| Access Restriction | Open |
| Subject Keyword | Type Checking Type Rule Model Checker Type System Data Flow Analysis Verified Compiler Attribute-labelled Control Flow Graph Verified Optimization Data-flow Analysis Complex Analysis Alternative Logic Compiler Optimization Data-flow Analysis-based Optimization Control Flow New Construct Specified Analysis Single Declarative Framework Key Word Abstract Syntax Tree Attribute Grammar Verified Data-flow Analysis-based Optimization Attribute Grammar Specification Language Program Optimization Community Developed Tool Different Temporal Logic Ltl-fv Formula Different Program Representation High-confidence Language Implementation Automated Proof Tool Optimization Verification Program Dependency Graph |
| Content Type | Text |
| Resource Type | Article |
