Semantik och verifiering: Betydelse och korrekthet inom databehandling
Semantik handlar om den exakta innebörden av programmeringsspråk och andra notationer, till exempel designbeskrivningar. Semantik är viktigt för att exakt förstå och beskriva datorprogrammens beteende och säkerställa att de fungerar på samma sätt på olika datorplattformar.
Beskrivning
Verifiering handlar om att visa att det inte finns några buggar i program och att modeller av datorsystem är korrekta. Formell verifiering kan - i motsats till testning - i princip garantera att ett program fungerar korrekt.
Semantik och verifiering är av särskild betydelse för samtidiga och parallella system, eftersom sådana system är komplexa i sig själva och är benägna att begå misstag och svårfunna buggar. Ett bra exempel är minneshantering i flerkärniga processorer.
Vi utvecklar teorier och metoder för olika aspekter av semantik och verifiering. Formell logik och system för datorstödd matematisk bevisföring (teorembevisande system) är viktiga verktyg.
Forskningsämnen
- Parallella system
- Formella metoder
- Processkalkyl
- Programverifiering
- Semantik
- Testning
- Teorembevisning
- Svaga minnesmodeller
- Industriella tillämpningar
Seniora forskare
- Parosh Aziz Abdulla: semantics, program verification, concurrency
- Mohamed Faouzi Atig: program verification, weak memory models
- Johannes Borgström: semantics, program verification, process calculi
- Lars-Henrik Eriksson: formal methods methodology, industrial applications
- Bengt Jonsson (se ävem hans hemsida): semantics, program verification, concurrency
- Joachim Parrow (se även hans hemsida): process calculi
- Björn Victor: process calculi
- Tjark Weber (se även hans hemsida): theorem proving
Forskningspriser
- CAV Award 2017: Parosh Aziz Abdulla och Bengt Jonsson
- LiCS Test-of-Time Award 2016: Parosh Aziz Abdulla och Bengt Jonsson