The Taub Faculty of Computer Science Events and Talks

This work uses static data and control flow code analysis to aid in proving properties of systems with aspects. Some new categories of aspect advices (code segments) and introduced methods are defined, beyond the existing ones. The categories are chosen considering their effectiveness, in that they both provide real aid in verification of properties, and are automatically detectable using data and control flow. The theoretical part of the thesis investigates which linear temporal logic properties of a system are maintained when an aspect from the newly defined category is added. In the practical part of the work, an automatic tool based on forward flow analysis for the detection of the categories is built, and applied to benchmark aspect systems.