A Modular Rewriting Approach to Language Design, Evolution and Analysis

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.The research in this dissertation has been supported in part by NSF grants CCF-0448501, CNS-0509321 and CNS-0720512, by NASA contract NNL08AA23C, by the Microsoft/Intel funded Universal Parallel Computing Research Center at UIUC, and by several Microsoft gifts.unpublishednot peer reviewe