|
Award Abstract #0811665
CPA-SEL-T: Domain Specific Languages, Logics, and Proofs for Certified Software Design
| NSF Org: |
CCF
Division of Computer and Communication Foundations
|
|
|
| Initial Amendment Date: |
July 16, 2008 |
|
| Latest Amendment Date: |
May 8, 2009 |
|
| Award Number: |
0811665 |
|
| Award Instrument: |
Continuing grant |
|
| Program Manager: |
Sol J. Greenspan
CCF Division of Computer and Communication Foundations
CSE Directorate for Computer & Information Science & Engineering
|
|
| Start Date: |
July 1, 2008 |
|
| Expires: |
June 30, 2010 (Estimated) |
|
| Awarded Amount to Date: |
$622496 |
|
| Investigator(s): |
Zhong Shao shao@cs.yale.edu (Principal Investigator)
Paul Hudak (Co-Principal Investigator)
|
|
| Sponsor: |
Yale University
P.O. Box 208337
NEW HAVEN, CT 06520 203/432-2460
|
|
| NSF Program(s): |
SOFTWARE & HARDWARE FOUNDATION,
SOFTWARE FOR REAL-WORLD SYSTMS,
COMPUTING PROCESSES & ARTIFACT,
SOFTWARE ENGINEERING AND LANGU,
INFORMATION TECHNOLOGY RESEARC
|
|
| Field Application(s): |
0000912 Computer Science
|
|
| Program Reference Code(s): |
HPCC, 9251, 9218
|
|
| Program Element Code(s): |
7798, 7724, 7352, 2880, 1640
|
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.
Please report errors in award information by writing to: awardsearch@nsf.gov.
|
