Project title: Runtime verification
Dr. Zhijiang Dong

Runtime verification is a light-weight formal technique used to monitor and verify system behavior against given requirements during the execution of programs. Such requirements are typically specified by LTL-formulae (Linear temporal logic) or automata. One research topic is to develop techniques to guide the behavior of a program once its requirement is violated. Another possible topic is the extension of aspect-oriented programming language (such as AspectJ) to provide solutions to program guidance.