ABSTRACT Verifying Aspect Advice Modularly ∗

Aspect-oriented programming has become an increasingly important means of expressing cross-cutting program abstractions. Despite this, aspects lack support for computeraided verification. We present a technique for verifying aspect-oriented programs (expressed as state machines). Our technique assumes that the set of pointcut designators is known statically, but that the actual advice can vary. This calls for a modular technique that does not require repeated analysis of the entire system every time a developer changes advice. We present such an analysis, addressing several subtleties that arise. We also present an important optimization for handling multiple pointcut designators. We have implemented a prototype verifier and applied it to some simple but interesting cases