Compositional Correctness: The Road Ahead
Abstract
Verifying the correctness of a complete software-reliant system is notoriously complex. Unfortunately,we face this complexity not only the first time we develop the system but every time we modify it. Thisis a daunting task because software needs to be continuously modified to accommodate new featuresover its lifetime. Compositional correctness (CC) is an area of research that takes advantage of the factthat software is developed as a set of interconnected modules. In a nutshell, CC focuses on provingproperties of individual modules (that are simpler to tackle) and composing the properties of all themodules into system-wide properties.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 2020
- Accession Number
- AD1130293
Entities
People
- Edward Desautels
Organizations
- Carnegie Mellon University