A modular rewriting approach to language design, evolution and analysis

Hills, Mark

Permalink

https://hdl.handle.net/2142/14600 Copy

Description

Title

A modular rewriting approach to language design, evolution and analysis

Author(s)

Hills, Mark

Issue Date

2010-01-06T16:13:44Z

Director of Research (if dissertation) or Advisor (if thesis)

Rosu, Grigore

Doctoral Committee Chair(s)

Rosu, Grigore

Committee Member(s)

• Gunter, Carl A.
• Kamin, Samuel N.
• Meseguer, José
• Mosses, Peter D.

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• language prototyping
• language semantics
• rewriting logic
• rewriting logic semantics
• program analysis
• modular language definitions

Abstract

Software is becoming a pervasive presence in our lives, powering computing systems in the home, in businesses, and in safety-critical settings. In response, languages are being defined with support for new domains and complex computational abstractions. The need for formal techniques to help better understand the languages we use, correctly design new language abstractions, and reason about the behavior and correctness of programs is now more urgent then ever. In this dissertation we focus on research in programming language semantics and program analysis, aimed at building and reasoning about programming languages and applications. In language semantics, we first show how to use formal techniques during language design, presenting definitional techniques for object-oriented languages with concurrency features, including the Beta language and a paradigmatic language called KOOL. Since reuse is important, we then present a module system for K, a formalism for language definition that takes advantage of the strengths of rewriting logic and term rewriting techniques. Although currently specific to K, parts of this module system are also aimed at other formalisms, with the goal of providing a reuse mechanism for different forms of modular semantics in the future. Finally, since performance is also important, we show techniques for improving the executable and analysis performance of rewriting logic semantics definitions, specifically focused on decisions around the representation of program values and configurations used in semantics definitions. The work on performance, with a discussion of analysis performance, provides a good bridge to the second major topic, program analysis. We present a new technique aimed at annotation-driven static analysis called policy frameworks. A policy framework consists of analysis domains, an analysis generic front-end, an analysis-generic abstract language semantics, and an abstract analysis semantics that defines the semantics of the domain and the annotation language. After illustrating the technique using SILF, a simple imperative language, we then describe a policy framework for C. To provide a real example of using this framework, we have defined a units of measurement policy for C. This policy allows both type and code annotations to be added to standard C programs, which are then used to generate modular analysis tasks checked using the CPF semantics in Maude.

Graduation Semester

2009-12

Permalink

http://hdl.handle.net/2142/14600

Copyright and License Information

Copyright 2009 Mark A. Hills

Owning Collections