Tools and Methods for Scalable Software Verifications

  • Sestoft, Peter (CoI)
  • Birkedal, Lars (PI)
  • Mehnert, Hannes (CoI)
  • Jensen, Jonas Buhrkal (CoI)
  • Bengtson, Jesper (CoI)
  • Thamsborg, Jacob Junker (CoI)
  • Hartmann Jensen, Mads (CoI)
  • Sieczkowski, Filip (CoI)
  • Mehnert, Hannes (CoI)
  • Svendsen, Kasper (CoI)

    Project: Research

    Project Details

    Description

    The need for correct and reliable software pervades all branches of society, such as telecommunications, manufacturing, trade, healthcare, finance, defense, and research. While software correctness has many facets (usability, security, and so on), this project focuses on functional correctness of sequential programs.

    The last 50 years have shown how difficult it is to construct software that works correctly. In the last 40 years researchers have endeavored to develop program logics for formal specification of software's intended behavior and to prove that it satisfies the specification.

    So-called shared mutable data have proven to be especially problematic, yet are ubiquitous in widely use programming languages such as Java and C#. It is hard to express properties of such software and it is hard to conduct proofs about it.

    In recent years progress has been made on two fronts: the development of program logics, notably separation logic, and the development of proof assistants. Separation logic allows one to focus a proof on only the relevant substructures of shared mutable data, but so far only smallish "toy" programs have been specified and proven using separation logic.

    The goals of this project are therefore:
    - To apply the above-mentioned theoretical advances to practice
    - To develop prototype software tools for formal specification with separation logic
    - To apply the prototypes in a realistic case study
    - To give methodological advice on how to structure software so as to facilitate formal specification and proof about it, and give advice on how to conduct such proofs.
    AcronymToMeSo
    StatusFinished
    Effective start/end date01/03/200930/06/2013

    Funding

    • Independent Research Fund Denmark: DKK5,394,541.00

    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.
    • A Concurrent Logical Relation

      Birkedal, L., Sieczkowski, F. & Thamsborg, J. J., 2012, In: Dagstuhl Seminar Proceedings. 16, 21 p.

      Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

      Open Access
      File
    • Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant

      Mackay, J., Mehnert, H., Potanin, A., Groves, L. & Cameron, N., 2012, FTfJP 12.Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs . Association for Computing Machinery, p. 11-19 8 p.

      Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

      File
    • Formalized Verification of Snapshotable Trees: Separation and Sharing

      Mehnert, H., Sieczkowski, F., Birkedal, L. & Sestoft, P., 2012, Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings. Springer, Vol. 7152. p. 179-195 15 p. (Lecture Notes in Computer Science, Vol. 7152).

      Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

      File