CAREER: Formal Verfication of Aspect-Oriented Software

Brown University, Providence RI

Investigators

Abstract

ABSTRACT 0447509 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.