PP-K: Scaling by Decomposition

The goal of this project is to make the verification of re-engineered programs scale. We will reduce conceptual complexity by compositional reasoning. More specifically, compositional reasoning will happen by exploiting design patterns introduced during the re-engineering process. We will develop a portfolio of compositionality results that allow one to deduce guarantees for a complex program from properties of its components. Formal semantics and verification will be employed to ensure high reliability. Rely-guarantee reasoning will be employed to ensure high precision of the compositional analysis. We will evaluate our approach and results at realistic programs, including the HPC applications provided by Part Project P.
PPK Workflow
You should have a solid background in at least one of the following areas:

  • formal methods in Computer Science or mathematical logic
  • semantics of concurrent programs or weak memory models
  • program analysis or transformation techniques
  • use of verification tools like Isabelle/HOL or Coq