SHF: Small: Collaborative Research: Specification Language Foundations for Modular Reasoning Methodologies

Project: Research project

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.

StatusFinished
Effective start/end date1/08/0931/07/12

Funding

  • National Science Foundation

Fingerprint

Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.