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.
Writing correct, robust, and efficient software is a famously difficult problem. Software defects have led to many disastrous outcomes that have caused huge financial losses, serious compromises of privacy, physical systems failures, and insidious threats to national security. The goal of this project is to improve the software development process to ensure that our programs are correct, according to a given specification, at the time that we construct them. Testing a software system is not good enough, since testing can never cover all possible execution sequences of a program. Instead, a formal proof is needed to assure correctness of a program with respect to a specification. Our research has focused on achieving this goal through the development of new programming languages that are more abstract and better able to express concisely and accurately a problem solution. These languages are often called "domain specific" in that they are designed for a particular application domain. In addition, we have developed new automated proof techniques to ensure that a program meets a desired specification. A key application area of our research is the desigh of certifiably correct low-level operating systems code -- that is, the program that runs the core of an operating system such as Windows, Mac OS, and so on. These operating systems are deceptively complex, and notorious for their vulnerabilities. To support large-scale proof development, we have developed a new general-purpose programming languaged (named VeriML) that aims to fix several architecture-level deficiencies in existing proof assistants. We have also designed and implemented a few new domain specific program logics for reasoning about low-level and concurrent code at different abstraction layers. These new technologies together forms the core of our new certified software methologies for developing domain-specific languages, logics, libraries, and proofs.
