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)

    Projekter: ProjektForskning

    Projektdetaljer

    Beskrivelse

    De sidste 50 år har vist at det er særdeles vanskeligt at konstruere software der fungerer korrekt. I 40 år har man forsøgt at udvikle programlogikker til formel specifikation og bevisførelse for softwarekorrekthed. Såkaldte delte opdaterbare

    datastrukturer, der gennemsyrer moderne programmeringssprog såsom Java og C#, er særlig problematiske, både hvad angår at udtrykke funktionelle egenskaber og at gennemføre beviser om dem.



    De seneste år er der gjort fremskridt i udviklingen af både programlogik og bevisværktøjer. Med separation logic, udviklet af Reynolds og O'Hearn, kan man fokusere et bevis på relevante delstrukturer, hvilket letter beskrivelse af delte

    opdaterbare datastrukturer meget betydeligt. Imidlertid er separation logic indtil videre kun anvendt på mindre eksempler.



    Måler med dette projekt er

    (1) at bringe de nævnte teoretiske landvindinger nærmere til praksis,

    (2) at konstruere prototyper af softwareværktøjer til formel specifikation med separation logic

    (3) at afprøve prototypen på et realistisk case study

    (4) at give metodiske anvisninger til softwarekonstruktion så det er nemmere at formulere og vise egenskaber.



    Det påtænkte case study er et softwarebibliotek som er væsentligt fordi det bruges i praksis, udfordrende på grund af dets kompleksitet, og velegnet fordi dets struktur muliggør en trinvis tilgang til udfordringerne.



    Projektet vil kombinere vores ekspertiser i moderne programmeringssprog og udviklingsmiljøer, og i det teoretiske grundlag for programlogik.

    AkronymToMeSo
    StatusAfsluttet
    Effektiv start/slut dato01/03/200930/06/2013

    Finansiering

    • Danmarks Frie Forskningsfond: 5.394.541,00 kr.

    Fingerprint

    Udforsk forskningsemnerne, som dette projekt berører. Disse etiketter er oprettet på grundlag af de underliggende bevillinger/legater. Sammen danner de et unikt fingerprint.
    • A Concurrent Logical Relation

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

      Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

      Åben adgang
      Fil
    • 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, s. 11-19 8 s.

      Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

      Fil
    • 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, Bind 7152. s. 179-195 15 s. (Lecture Notes in Computer Science, Bind 7152).

      Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

      Fil