Det är illa nog att förlora en timmes arbete när din dator kraschar — men i inställningar som sjukvård och flyg, programvarufel kan få mycket allvarligare konsekvenser. I ett ökänt fall, ett datorfel fick cancerpatienter att få dödliga överdoser från en strålbehandlingsmaskin; i nyare rubriker, bristfällig programvara fick skulden för flygplanskrascher i Etiopien och Indonesien.

Nu forskare vid Stevens Institute of Technology, i samarbete med Yale University, utvecklar verktyg som kan göra katastrofala datorolyckor mycket mindre sannolika. Leds av Eric Koskinen, en biträdande professor i datavetenskap vid Stevens, arbetet syftar inte bara till att se till att programmen fungerar korrekt i specifika situationer, men använder också algoritmer för att avgöra om det är logiskt möjligt, under alla omständigheter, för programvara för att ge oönskade resultat.

"Vad vi siktar på är en 100-procentig garanti att du aldrig kommer att stöta på en bugg, sa Koskinen.

Koskinens team, med över 2,5 miljoner dollar från Office of Naval Research, modellerar skillnader mellan två versioner av ett program. Det är användbart eftersom programmerare ofta arbetar genom att bygga på befintlig programvara, istället för att skriva kod från början, och buggar kan introduceras från en version till nästa. Detta tillvägagångssätt är särskilt värdefullt för militären, eftersom försvarsbyråer ofta köper programvara från privata entreprenörer, gör sedan ändringar internt innan du använder dem i uppdragskritiska situationer.

"De behöver ett sätt att bekräfta att de har gjort ändringar på rätt sätt internt, och har inte introducerat nya problem, " sa Koskinen.

För att matematiskt bevisa att ett datorprogram aldrig skulle kunna ha någon form av bugg, oavsett omständigheter, förutsedda eller oanade, Koskinens team använder en strategi som kallas tidslogik. Istället för att granska enskilda rader kod för att leta efter syntaktiska skillnader, laget, inklusive biträdande professor Jun Xu, en expert på binär analys på Stevens, tittar på hur ett program beter sig över tid. Tanken är att bevisa att oavsett hur länge programmet pågår, det finns inget logiskt sätt för det någonsin att returnera ett oönskat resultat.

Modellera ett programs struktur och beteende, snarare än att titta på enskilda rader kod, är viktigt eftersom exakt samma kodrader kan ha olika effekter i olika sammanhang, precis som rader kod som ser väldigt olika ut kan åstadkomma samma sak. Det är som att studera ett juridiskt dokument, Koskinen förklarar:att ändra ett enda ord kan tyckas trivialt, men kan ändra hela innebörden av dokumentet. Temporal logik hjälper till att modellera ett programs potential, få kraftfulla insikter i programmets verkliga möjligheter.

Teamets tillvägagångssätt gör det också möjligt att eliminera buggar i kommersiell programvara från hyllan där källkoden inte är tillgänglig. Utan källkoden, teamet får jämföra datorprogram med den binära versionen av källkoden. "Det är svårt att se om sårbarheten verkligen har eliminerats om du inte kan se källkoden, " sa han. "De tekniker vi bygger kommer att göra det:om du har en version av programvaran som du litar på, Våra tekniker kommer att kunna hjälpa dig att upptäcka förändringar – sårbarheter i programuppdateringar eller skadlig programvara som infogas i körbara program – och bestämma om du ska lita på den nya versionen."

Koskinens team håller också på att utveckla en verktygslåda som andra forskare och allmänheten kommer att kunna använda för att testa mjukvara – och de skalar upp sin metod för att arbeta med större program och mer komplexa problem. "Det här är stora problem som plågar moderna datorsystem, ", sa Koskinen. "De här frågorna kommer bara att bli mer kritiska – inom områden som sjukvård, flyg, autonoma fordon, och många fler – så det är viktigt att vi utvecklar praktiska tekniker för att göra datorstyrda system felfria och säkra att använda."