CPA-SEL-T: Domain Specific Languages, Logics, and Proofs for Certified Software Design

Yale University, New Haven CT

Investigators

Abstract

This research focuses on developing a new programming methodology to dramatically improve the quality and dependability of software-intensive systems. The key to this effort is an effective integration of domain-specific languages (DSLs) and formal program verification, two well-known technologies that have been used extensively on their own, but mostly in isolation of one another. DSLs make it easier to write complex software for specific application domains, but they often lack rigorous semantics, making it difficult to formally specify and reason about the resulting programs. Existing program verification systems, on the other hand, usually rely on a single unified logic (e.g. Hoare logic) or type system, which cannot support the diversity of components in typical software-intensive systems. By combining the two methodologies, the PI intends to resolve both of these shortcomings. More specifically, the PIs propose to develop a new DSL-centric certified software design methodology that will elevate existing DSL practice into a rigorous software development methodology that allows program verification to scale effectively to large software systems. The proposed research will impact the software engineering community and make it possible to build software more quickly, and with higher assurance of correctness, than previously possible.