Hoppa till innehåll
EN In english

Pålitlig mjukvara via programmering och kompilering i logik

Diarienummer
FFL15-0191
Projektledare
Myreen, Magnus
Start- och slutdatum
170101-211231
Beviljat belopp
12 000 000 kr
Förvaltande organisation
Chalmers University of Technology
Forskningsområde
Informations-, kommunikations- och systemteknik

Summary

Objective The objective of this project is to turn interactive theorem provers into highly trustworthy programming environments. Most software is littered with flaws. Certain software is not allowed to contain flaws, e.g. the software in your (self-driving) car. This type of software is called high-assurance software and is traditionally prohibitively expensive to develop to the necessary levels of quality. Results The proposed project will make significant contributions to the development of high-assurance software. The proposed work will make it easier to write software in proof assistants and to prove that the software respects a precise specification. This project will take Sweden to the cutting edge of high-assurance software development. Plan The work will build on my extensive experience in interactive theorem proving and particularly my experience in proof methods for connecting machine code with functional programming. The project will be pursued in three parts that run in parallel. My group will: - explore how logic and proof automation can be used for programming in a combination of different programming styles: functional, imperative, assembler; - develop new proof methods with logical foundations that are well beyond the current state of the art; - construct a theory for proved-correct just-in-time compilation within proof assistants.

Populärvetenskaplig beskrivning

Vi använder en massa datorer i vårt dagliga liv. Vi är beroende av våra telefoner och är villiga att ge dem våra bankuppgifter. Vi kör bil och snart kommer bilarna kanske att köra sig själv. Ett ökande antal människor har datorer som en del av sin kropp: pacemakers, hörapparater, insulinpumpar, och så vidare. Trenden är att sätta allt mer avancerade programvara i vardagsföremål. Denna programvara är av varierande kvalitet. Under vissa omständigheter, vill vi veta programmen inte har fel, och att det alltid kommer att bete sig som förväntat. Detta projekt kommer att utveckla vetenskapen bakom byggandet av programvara som är garanterad att inte har vissa typer av fel. Detta projekt kommer att utveckla metoder genom vilka matematiska bevis kan användas för att bevisa att programvaran alltid beter sig enligt programmerarens förväntningar. Detta projekt kommer att fokusera på metoder för programkonstruktion inom verktyg för utveckling av matematiska bevis. Detta projekt kommer att göra dessa verktyg användbara för programmering. Projektet kommer att betona de matematiska grunderna för dessa verktyg så att vi kan ha så mycket förtroende för resultaten som möjligt.