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.