Traver: Taming memory models

Traver stands for Transformation Verification. The goal of the Traver project is to help programmers and compiler writers to understand the precise implications of program transformations of concurrent programs. Of particular interest are the effects of relaxed memory models, and how they impact the correctness of translations.

Who cares?

Compiler writers in particular are faced with the challenges of (1) ensuring that optimizations do not alter the program behavior, and (2) correctly expressing language-level synchronization (such as locks, volatiles, or interlocked operations) using hardware-level operations (as supported by the targeted platform).

What can Traver do for you?

The Traver project assists compiler writers and programmers as follows.

  • We provide a rigorous theoretical foundation to prove correctness of program transformations.
  • We provide a semi-automatic tool to assist with proving or refuting correctness.
Publications