Vårt uppdrag
Mjukvarukorrekthet gjord hanterbar
På Syntemantic anser vi att programvara bör vara matematiskt rigorös. Att bevisa korrekthet för varje system är dock komplicerat och opraktiskt. Det är också otillräckligt, eftersom oväntade fall kan uppstå i praktiken. Därför tillämpar vi matematiska metoder som ger korrekthetsgarantier på ett mätbart, reproducerbart och effektivt sätt. Med hjälp av dessa metoder kan vi generera en mängd möjliga utfall och identifiera luckor i testningen, utan att kräva manuell, uttömmande granskning.
Vår historia
Syntemantic grundades på idén att programvara bör bete sig i enlighet med både mänskliga specifikationer och maskininstruktioner. I praktiken är dock inte detta tillräckligt, eftersom de antaganden som görs vid programmering ofta skiljer sig från de som används i ett formellt bevis. Under senare år har det skett stora framsteg inom datorstödda bevisspråk, så kallade 'bevisassistenter', som kan verifiera kod med hjälp av typteori, vilket gör att programmet i praktiken fungerar som sitt eget bevis. Många matematiska satser har till exempel redan formaliserats i bevisassistenten Lean, även om mycket arbete återstår. Tyvärr kan inte alla datorprogram enkelt formaliseras och översättas till Lean. Vi är övertygade om att vi, genom väldefinierade specifikationer och korrekt testdesign, kan använda matematiska metoder för att generera en lämplig testsvit som matchar givna kriterier. Dessa kriterier varierar beroende på programvarans art; säkerhetskritiska system har exempelvis betydligt strängare krav än ett kontaktformulär på en webbplats. Genom att definiera storleken och geometrin på testrymden, samt begränsa den utifrån praktiska förutsättningar som tid och beräkningsresurser, kan vi fatta smartare, datadrivna beslut vid utveckling av programvara.