Integrating Temporal Specifications as Runtime Assertions into Parallel Debugging Tools

Research and Development Goals Debugging nondeterministic parallel programs is a difficult and tedious task. In this project we propose to investigate the use of program specifications, which can serve as enhanced debugging aids in existing parallel debugging tools. The principal idea is to formulate a specification of expected program behavior, translate this specification into runtime assertions, and check them during execution. With this sophisticated approach, the user may select a subset of all possible executions on which checking should be performed and collect for each check a consistent global state of the observed application.