KTH-avhandling gav tungt pris

Det räcker inte med att testa om datorsystemet verkar fungera – i många fall måste det gå att garantera att inga fel kan uppstå. Om till exempel datorn i autopiloten på en jumbojet hänger sig får det förödande konsekvenser.

För att göra det används matematiska verktyg och datorberäkningar för att bevisa att system är felfria.

Men formlerna kan vara ohyggligt stora med miljontals variabler, och länge har processorkraft och minnesanvändning varit en flaskhals. Om minnesmängderna blir för stora kan det bli svårt att hitta den nål i höstacken som beviset är.

En naturlig strategi att lösa detta på har varit att begränsa minnesanvändningen, men det kan få dramatiska konsekvenser för hur lång tid beräkningarna tar. Det visar Jakob Nordströms forskning som ingår i en avhandling som lades fram vid KTH under förra året.

- Vi har bevisat matematiskt att det är en delikat balansgång mellan processorkraft och minne, säger Jakob Nordström, i dag forskare vid det amerikanska universitetet Massachusetts Institute of Technology, MIT.

Han tillägger att gränsen är hårfin.

- Skillnaden mellan att en uträkning bara tar några sekunder och i stället breder ut sig över tusentals år är extremt liten, säger Jakob Nordström.

Det är för den här forskningen som han får Ackermann Award 2009, som delas ut av European Association for Computer Science Logic till "enastående avhandlingar i datavetenskaplig logik". Tidigare år har priset delats mellan flera avhandlingar, men i år är Jakob Nordström ensam pristagare.

Jakob Nordström arbetar med grundforskning, men de resultat som hans forskning genererat kan ha stor praktisk nytta inom industrin.

Tar en uträkning för lång tid kan det sluta med system som inte håller måttet.

Sin forskartjänst vid MIT kommenterar han på följande sätt.

- Min avhandling vid KTH var helt klart en av anledningar till att jag var välkommen till MIT, säger Jakob Nordström.

Peter Larsson