Modular Reasoning about Software

    Project: Research

    Project Details

    Description

    For almost 40 years, computer science researchers have hoped to be able to mathematically verify properties of software. Despite a lot of research effort, most tools used in practice can still only verify simple properties. In particular, it has proved very difficult to develop tools to verify non-trivial properties of programs that use references to shared mutable data, ubiquitous in modern object-oriented languages. The consequence is that the developed tools will only work on small programs.

    The goal of this project is to investigate and develop theories and methods for modular reasoning about software written in modern programming languages. The purpose is to lay the foundation for improvement of software tools, which are being and will be developed over the next five to ten years and which will be used to improve software practice. This is very important for society because software errors are extremely costly and can have fatal consequences.
    AcronymMoReSo
    StatusFinished
    Effective start/end date01/01/200831/12/2011

    Collaborative partners

    • IT University of Copenhagen (lead)
    • Carnegie Mellon University (Project partner)
    • University of Cambridge (Project partner)
    • Queen Mary and Westfield College (Project partner)
    • Harvard University (Project partner)
    • Microsoft Research (Project partner)
    • University of Copenhagen (Project partner)
    • Stevens Institute of Technology (Project partner)
    • University of Sussex (Project partner)
    • University of Birmingham (Project partner)
    • University of Edinburgh (Project partner)

    Funding

    • Independent Research Fund Denmark: DKK3,810,715.00

    Keywords

    • Modular Reasoning

    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.