Theory, in Practice

Specifying and checking stateful software interfaces Manuel Fähndrich
Mainstream software interfaces describe types, sets of accessible functions, fields, and the expected and returned types of such operations. They lack any indication of requirements or effects on the underlying state of the system. Since most programming environments are stateful, important data and control invariants are not specified. This lack of stateful specifications opens up these systems to a myriad of reliability problems that manifest in possible runtime failures. In these lectures we will examine how advanced type systems based on forms of linear logic can capture many such stateful invariants concisely and naturally. We will describe how such systems can be integrated in novel programming language or existing language extension and some experience with several systems we built in the past .

Improving Software Quality with Type Qualifiers Jeff Foster
Software continues to increase in size and complexity, yet programmers have few practical tools and techniques to ensure its quality and reliability. In these lectures, we will explore a general technique based on type qualifiers that allows programmers to write annotations in their source code describing additional program properties that should be maintained during execution. Type qualifiers have a number of advantages as a mechanism for specifying and checking properties of programs: They are a simple, natural extension of the standard types present in typical programming languages; they support efficient inference algorithms, so that programmers need only write a few annotations and the rest are inferred automatically; and the results of type qualifier inference can be intuitively presented to the programmer to justify any errors that are detected.

We will discuss theoretical foundations and practical implementation issues for type qualifiers, including efficient inference algorithms that scale to large programs such as the Linux kernel. We will also discuss particular issues in adding type qualifiers to C. We will discuss examples of qualifiers, such as ANSI C's const , security-related qualifiers for finding format-string vulnerabilities , and qualifiers to support transparent proxies in Java . If time permits, we will also discuss qualifiers for deadlock detection in the Linux kernel.

Domain-Specific Languages: For Fun and Profit Kathleen Fisher
Domain-specific languages can dramatically improve the reliability of software by providing highly-tailored abstractions. Such abstractions can significantly reduce code sizes, making maintenance easier. In addition, tricky or extensive "boilerplate" code can be generated by the compiler rather than hand-coded, making user-code more reliable. (Presumably the compiler-writers know what they are doing, or at least, the code can be debugged once and then reused by many!) An additional benefit of domain-specific languages is that they provide an opportunity for programming languages research to affect other aspects of computer science in a much shorter time-frame than general purpose languages can. This immediacy makes programming language work obviously relevant to our colleagues, provides a wonderful platform for experimenting with language technology, and poses new research challenges.

This series of talks will describe two different domain-specific languages that have been developed at AT&T. Each of these languages endeavors to improve the reliability of software and have an immediate impact on a user group. The first of these languages, Hancock , facilitates writing programs to construct and maintain "customer" profiles from high-volume transactional data streams. Hancock programs have been used in production fraud and marketing applications for several years to significant financial effect. The second language, PADS , allows users to describe ad hoc data declaratively, including physical layout information and semantic constraints. The PADS compiler then generates a library and various tools for parsing and manipulating the data. In the talks, we will motivate the need for Hancock and PADS, describe and evaluate the designs, discuss their use at AT&T, and point out possible areas for future research.


This page is the property of the University of Oregon