Project Details
Description
This project extends the semantical foundations of object-oriented (OO)
languages to cover methodologies for modular reasoning. Modular reasoning
means verifying software components assuming the specification of each
used component. Modularity is important for productivity and scalability,
but is difficult to achieve for OO software. To support modular reasoning,
researchers have proposed several methodologies that restrict programs and
their specifications. The goal of this project is to provide a theoretical
basis that supports practical techniques for justifying and using
methodologies.
This project provides guidance for the designers of programming and
specification languages, verification logics, and associated tools. The
results will improve the utility and extensibility of verification tools
--- a key goal of the Verified Software grand challenge. Software
developers may benefit from the integration and harmonious interoperation
of best-practice methodologies. This project is potentially
transformative: it aims to enable combinations and customizations of
methodologies by tool users, scalable to real applications.
Improved OO programming methodologies may greatly improve programming
practice, especially in applications needing high assurance, reliability,
and security. This will benefit society, which increasingly depends on
computing systems built using OO components. Unification of methodologies
and streamlining of tools also facilitates the education of software
developers.
Status | Finished |
---|---|
Effective start/end date | 1/08/09 → 31/07/12 |
Funding
- National Science Foundation