Doktorand i datalogi med fokus på automatiserad verifiering av numerisk kod - Under tillsättning eller tillsatt, ej sökbar

Vill du arbeta med automatiserad programverifiering, med stöd av kompetenta kollegor i en ledande internationell miljö? Vill du ha en arbetsgivare som satsar på ett hållbart medarbetarskap och erbjuder trygga, förmånliga arbetsvillkor? Välkommen att söka anställning som doktorand på Uppsala universitet. 

Institutionen för informationsteknologi har en ledande position inom såväl forskning som utbildning på alla nivåer. Vi är idag Uppsala universitets tredje största institution och har i dag drygt 350 anställda varav 120 är lärare och 120 är doktorander. C:a 5000 grundutbildningsstudenter läser en eller flera kurser vid institutionen varje år. Mer information om oss hittar du på institutionen för informationsteknologis webbplats.

Doktorandtjänsten är på avdelningen för datalogi, specifikt inom programspråksgruppen som för närvarande består av 6 seniora forskare och 7 doktorander som arbetar med olika aspekter av programspråksdesign och verifiering. Utöver tekniska samarbeten träffas gruppen regelbundet och erbjuder en engagerande och stödjande miljö.

Projektbeskrivning
Numerisk programvara används i stor utsträckning för att modellera, simulera, förutsäga och fatta beslut i applikationer inom olika domäner som dataanalys, väderprognoser, fysik och teknik. Att säkerställa att sådan programvara är korrekt är viktigt, men inte trivialt. Ett sätt att göra det är att använda rigorös automatiserad verifiering som bevisar vid kompilering att ett program för alla giltiga indata beräknar vad det förväntas göra. Emellertid är automatiserad verifiering av numeriska program över ändlig precision (t.ex. flyttal) för närvarande begränsad. Ändlig precision introducerar avrundningsfel med avseende på en idealisk realtalsspecifikation och ställer unika utmaningar för verifiering av programnoggrannhet och andra typer av önskvärda egenskaper.

Målet med detta avhandlingsprojekt är att utveckla en rigorös verifieringsmetod och verktyg för existerande numerisk programvara. Projektet kommer att utforska, utveckla och kombinera olika statiska och dynamiska verifieringstekniker med den slutliga ambitionen att göra det lättare för utvecklare att skriva korrekt numerisk kod. De utvecklade teknikerna kommer att implementeras i ett praktiskt användbart verktyg, och kan till exempel bygga på LLVM-ramverket.

Arbetsuppgifter
Doktoranden ska främst ägna sig åt den egna forskarutbildningen. Övrig tjänstgöring vid institutionen, som avser undervisning och administrativt arbete, kan ingå inom ramen för anställningen (max 20%).

Kvalifikationskrav
Behörig till utbildning på forskarnivå är den som har

• avlagt examen på avancerad nivå inom datavetenskap eller inom ett liknande område, eller
• fullgjort minst 240 högskolepoäng, varav minst 60 högskolepoäng på avancerad nivå inklusive ett självständigt arbete om minst 15 högskolepoäng, eller
• på något annat sätt förvärvat i huvudsak motsvarande kunskaper.

Vi söker kandidater med

• en stark matematisk bakgrund och intresse för statisk och/eller dynamisk programanalys, programspråkstekniker eller formell verifiering,
• utmärkt kommunikationsförmåga med tillräckliga kunskaper i muntlig och skriftlig engelska,
• goda kunskaper i programmering och problemlösning,
• förmåga att arbeta väl både på egen hand och tillsammans med andra i en blandad grupp.

Önskvärt/meriterande i övrigt
Erfarenhet och kurser inom ett eller flera ämnen är meriterande: statisk programanalys, dynamisk analys eller testning, programverifiering, programlogik, avancerad kompilatorkonstruktion.

Bestämmelser för doktorander återfinns i Högskoleförordningen 5 kap §§ 1-7 samt i universitetets regler och riktlinjer.

Ansökan
Ansökan ska innehålla:
1)    ett personligt brev (högst 2 sidor) där du kort motiverar varför du söker denna tjänst, som dessutom bör innehålla: a) kandidatens forskningsintressen, b) bevis på den sökandes egenmotivering och förmåga att arbeta i grupp, och c) en sammanfattning av dennes examensarbete eller ett jämförbart större projekt; 
2)    en meritförteckning (CV);
3)    examensbevis och registerutdrag med betyg (översatt till engelska eller svenska); 
4)    examensrapport (eller utkast till sådan, och/eller annan egenproducerad teknisk eller vetenskaplig text), publikationer och andra relevanta dokument; 
5)    Kontaktinformation för minst en referens (men inget referensbrev);
6)    Tidigast möjliga startdatum. 
 
Lovande sökande kommer att bjudas in till en intervju på plats innan de anställs.

Om anställningen 
Anställningen är tidsbegränsad, enligt HF 5 kap § 7. Omfattningen är heltid. Tillträde 1 september 2024 eller enligt överenskommelse. Placeringsort: Uppsala. 

Upplysningar om anställningen lämnas av: Universitetslektor Eva Darulova, e-mail: eva.darulova@it.uu.se.

Välkommen med din ansökan senast den 26 april 2024, UFV-PA 2024/957.