Shriram Krishnamurthi Brown University
CAREER: Formal Verification of Aspect-Oriented Software
Module systems have grown significantly in scope and sophistication. The most recent innovations have been in the space of so-called aspects, which provide modularity mechanisms that blur the line between static and dynamic composition. The creation of innovative module mechanisms gives programmers new powers, but in turn also makes it possible for them to introduce ever more subtle errors into software. This potential for new kinds of errors places a greater burden on verification techniques. These techniques have, however, failed to keep pace with advances in software modularity.
This proposal will advance the state of research in computer-aided verification for the forms of modularity introduced by aspects. It will generate new theories of modular verification that address the different styles of aspect modularities. This work is, therefore, an instance of a larger research program that seeks synergies in the confluence of software engineering, programming languages and computer-aided verification.
The proposal will also have significant broader impact. It will lead to tools that will benefit the software development community. It will generate a new design for programming languages courses. Finally, it will produce a course designed to teach computing to students of the social sciences.
Intellectual Merit: Executing the proposal resulted in both foundational results and new avenues of discovery. The work included a comprehensive account of verification for new forms of software modularity, providing a solid semantic foundation to work that had previously been handled informally; addressing better forms of program construction for Web applications; and the study of differential analysis for security and privacy policies. These results have been extensively documented in conference and journal papers spanning the areas of programming languages, software engineering, formal methods, and computer security. Most of these studies also resulted in software tools and benchmark suites, some of which are used extensively. Broader Impact: The work had educational impact in several forms. First, the PI helped create better and modern materials for the study of programming languages, and participated in research community efforts to modernize such education. Second, the PI jointly led the design of a new course of study in computing for humanities and social science students, resulting in technical exposure to what is now called ``big data'' (but had not yet been popularized at the time this work was envisioned). Finally, the proposal has trained numerous students at all levels from undergraduates to PhDs, who have gone on to successful careers in academia and industry.
