CAREER: Formal Verfication of Aspect-Oriented Software

Shriram KrishnamurthiBrown University CAREER：面向方面的软件模块系统的形式验证在范围和复杂性方面有了显著的增长。最新的创新是在所谓的方面领域，它提供了模糊静态和动态组合之间界限的模块化机制。创新模块机制的创建给程序员带来了新的力量，但反过来也使他们有可能在软件中引入更多微妙的错误。这种新类型错误的可能性给验证技术带来了更大的负担。然而，这些技术并没有跟上软件模块化的发展。这一建议将促进Aspects引入的模块化形式的计算机辅助验证的研究状况。它将产生新的模块验证理论，解决不同风格的方面模块。因此，这项工作是一个更大的研究项目的一个例子，该项目寻求在软件工程、编程语言和计算机辅助验证的融合中实现协同效应。该提案还将产生重大的更广泛的影响。它将产生使软件开发社区受益的工具。它将为编程语言课程产生一个新的设计。最后，它将推出一门旨在向社会科学学生教授计算机的课程。

ABSTRACT0447509Shriram KrishnamurthiBrown UniversityCAREER: Formal Verification of Aspect-Oriented SoftwareModule 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.