PP-K: Scaling by Decomposition

The goal of this project is to make the verification of re-engineered programs scale. We reduce conceptual complexity by compositional reasoning. More specifically, we enable compositional reasoning by exploiting design patterns introduced during the re-engineering process. We 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 are employed to ensure high reliability. Rely-guarantee reasoning is employed to ensure high precision of the compositional analysis. We evaluate our approach and results at realistic programs, including the HPC applications provided by Part Project P.
PPK Workflow