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

本研究的重点是开发一种新的编程方法，以显著提高软件密集型系统的质量和可靠性。这项工作的关键是领域特定语言（dsl）和正式程序验证的有效集成，这是两种众所周知的技术，它们各自被广泛使用，但主要是相互隔离的。dsl使得为特定的应用领域编写复杂的软件变得更加容易，但是它们通常缺乏严格的语义，使得很难正式地指定和推断结果程序。另一方面，现有的程序验证系统通常依赖于单一的统一逻辑（例如Hoare逻辑）或类型系统，它不能支持典型软件密集型系统中组件的多样性。通过结合这两种方法，PI打算解决这两个缺点。更具体地说，pi建议开发一种新的以DSL为中心的认证软件设计方法，将现有的DSL实践提升为严格的软件开发方法，允许程序验证有效地扩展到大型软件系统。所提出的研究将影响软件工程社区，并使更快地构建软件成为可能，并且具有比以前更高的正确性保证。

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.