University of Illinois Urbana-Champaign

A modular rewriting approach to language design, evolution and analysis

Hills, Mark

Content Files
Hills_Mark.pdf

Permalink

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

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
Date of Ingest
2010-01-06T16:13:44Z
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

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Siebel School of Computer Science