Doktorand i formell modellering och verifikation för hög tillförlitlighet

KTH svarar för en tredjedel av Sveriges kapacitet av teknisk forskning och ingenjörsutbildning på högskolenivå. Utbildningen och forskningen täcker ett brett område – från naturvetenskap till alla grenar inom tekniken samt arkitektur, industriell ekonomi och samhällsplanering. Totalt finns vid KTH 12 400 helårsstudenter på grundnivå och avancerad nivå, nästan 1900 aktiva forskarstuderande och 5100 anställda.

För mer information om skolan för datavetenskap och kommunikation, besök www.kth.se/csc.



Avdelningsinformation

Tjänsten hör till avdelningen för teoretisk datalogi, TCS, www.

csc.kth.se/tcs. Avdelningen har ca 40 lärare, forskare, och doktorander, och bedriver forskning inom grundläggande ämnen som komplexitetsteori, logik och formella metoder, såväl som mer applikationsorienterade ämnen som datasäkerhet och kryptografi, programmeringsspråk, databaser, naturliga språk, och datadidaktik. Inom datasäkerhet bedriver TCS-gruppen aktiv forskning inom mjukvarusäkerhet och säkra exekveringsplattformar, nätverkssäkerhet och kryptografi, särskild elektronisk röstning.

Arbetsuppgifter

Forskningsarbetet utförs i Prosper-gruppen, ett forskarteam som leds av professor Mads Dam med samarbetspartners vid SICS, Swedish Institute of Computer Science. För exempel på pågående projekt se prosper.sics.se och haspoc.sics.se. Vår forskningsvision är att producera högprestanda systemprogramvara för inbyggda system med matematisk garanterade säkerhetsegenskaper genom användningen av formell modellering och verifikation. Forskningen involverar design och implementation av olika typer av systemprogramvara, byggande av formella modeller för den underliggande hårdvara, samt utveckling av teorier och verktyg för verifikation av systemprogram.

Denna rekrytering är en del av vårt arbete på verifikation av systemmjukvara. Vi söker högt kvalificerade studerande som kan bidra till arbetet med formell modellering av processorer på mikroarkitekturnivå och verifikation av lågnivå kod. Den studerande kommer bli involverad i (i) modellering av lågnivå systemkomponenter med hjälp av interaktiva teorembevisare som HOL och Coq, (ii) validering av de formella modeller genom att jämföra modellernas beteende med riktig hårdvara och hårdvaruproducenternas informella specifikationer, samt (iii) användningen av de nya modeller till att verifiera effektiviteten och korrektheten av såväl nya som befintliga motmedel mot angreppsvektorer som involverar de modellerade systemkomponenterna.

Kvalifikationer

Kandidater för tjänsten förväntas vara, eller i närtid bli klar som civilingenjör eller masters i datalogi, datateknik, elektro, teknisk fysik, eller ett motsvarande ämne. Specialisering i ett eller flera områden relaterat till säkerhet, formella metoder, eller datorsystem, samt mycket god datorvana är viktigt.

Kandidaten bör ha excellenta akademiska meriter, och väl utvecklade analytiska problemlösningsfärdigheter. Vi söker en person med stark drivkraft inom området, som kan arbeta självständigt. Goda samarbets- och kommunikationsfärdigheter är viktiga. Goda kunskaper i engelska, både skriftlig och muntligt, är viktiga för att presentera sina resultat vid internationella konferenser och i internationella tidskrifter. Sådana kunskaper kan visas genom egenskrivet material, till exempel examensarbeten, eller språktester som TOEFL.

Fackliga representanter

Du hittar kontaktuppgifter till fackliga representanter på KTH:s webbsida. 

Ansökan

Ansökningen måste innehålla:

- CV inklusive relevant arbetslivserfarenhet och kunskap.
- Kopia på examensbevis samt utdrag av betyg från genomförda utbildningar på högskolenivå, med översättning till engelska eller svenska där detta är nödvändigt. Kopior av testresultat ska också bifogas.
- Ge en programförklaring: Varför vill du bli doktor, vilka är dina akademiska intressen och mål, hur relaterar de sig till dina tidigare studier; maximum 2 sidor.
- Publikationer och tekniska rapporter, ej längre än 10 sidor var. För längre dokument vänligen uppge URL och abstract.
- Rekommendationsbrev, alt. kontaktinformation, från två referenser.
Du ansöker via KTH:s rekryteringssystem. Du som sökande har huvudansvaret för att din ansökan är komplett när den skickas in.

Ansökan ska vara KTH tillhanda senast sista ansökningsdagen vid midnatt, CET/CEST (Central European Time/Central European Summer Time). 

Övrigt

Tjänsten avser en fyraårig tidsbegränsad plats, men kan vid max 20% institutionstjänstgöring, vanligtvis undervisning, förlängas ytterligare ett år. Forskarstuderande ska vara inskriven vid KTH och ansökan initieras vid erbjudande om anställning. Startdatum är öppet för diskussion. För mer information, besök våra sidor om doktorandstudier. Vi ser helst att anställningen kan börja under september 2016.

För mer information om doktorandstudier på KTH besök sidan Doctoral studies

Vi undanber oss direktkontakt med bemannings- och rekryteringsföretag samt försäljare av platsannonser.