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.
