Menu

Programmeringssprog og verifikation

Vi lever i dag i en verden hvor software er allestedsnærværende – lige fra den stationære pc til kontrol-software i et digitalur. Kompleksiteten af denne software bliver større og større, idet selv mobiltelefoner nu har næsten samme regnekraft og funktionalitet, som stationære computere havde for 5 år siden. Konstruktion af funktionel, stabil og anvendelig software er blevet en af de vigtigste udfordringer i ny produktudvikling.

Vores gruppe tager denne udfordring op ved at understøtte softwareudviklingsprocessen med mere kraftfulde analyseværktøjer og programmeringssprog baseret på et stærkt matematisk fundament. Hoveddisciplinerne til at understøtte denne tilgang er logik, formelle metoder, og automatiserede ræsonnementer, og vi bruger disse til at verificere og transformere programmer, samt til design og implementering af programmeringssprog.

Et af hovedpunkterne er udviklingen af automatiserede værktøjer, der kan verificere at et program skrevet i Java, Haskell, eller Prolog standser, dvs. at det ikke kører i en uendelighed. Vores tilgang er at oversætte de givne programmer til en grundlæggende beregningsmekanisme (omskrivning af termer) og fortsætte analysen der. På denne måde kan vores forskning i princippet anvendes på et vilkårligt program skrevet i et vilkårligt sprog.

Vi interesserer os også for analyse af, hvilke dele af koden, der kan nås, liveness og sikkerhedsegenskaber, bevisdeduktion, og forbedringer af statisk analyse og sprogimplementation.

Feltet for software verifikation kræver en kombination af mange discipliner (program-semantik, constraint solving, logik, effektive algoritmer, værktøjsintegration) og forskningen udføres derfor i tæt samarbejde med forskergrupper på andre universiteter og virksomheder:

- RWTH Aachen University, Aachen, Tyskland
- University of New Mexico, Albuquerque, USA
- Ben Gurion University, Beer-Sheva, Israel
- Eindhoven University of Technology, Eindhoven, Holland
- University of Innsbruck, Innsbruck, Østrig
- Katholieke Universiteit Leuven, Leuven, Belgien
- Microsoft Research, Redmond, USA
- Universidad Politecnica de Valencia, Valencia, Spanien

Videnskabelige medarbejdere
Peter Schneider-Kamp

Fabrizio Montesi

Luís Cruz-Filipe

Vi samler statistik ved hjælp af cookies for at forbedre brugeroplevelsen.  Læs mere om cookies

Acceptér cookies