CAREER: Formal Verfication of Aspect-Oriented Software

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

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.