Ramanathan Thinniyam Srinivasan

Kort presentation

Jag är biträdande professor vid Uppsala universitet och arbetar med programverifiering, särskilt för samtidiga och distribuerade system, samt kvantberäkning. För närvarande söker jag en doktorand för ett projekt om skalbar verifiering av kvantprogram, där metoder från programmeringsspråk, logik och formell verifiering kombineras.

Nyckelord

• programverifiering
• kvantdatorer
• samtidig programmering
• model checking
• programmeringsspråk.

Biografi

Jag är biträdande professor (tenure track) vid avdelningen för datorsystem vid institutionen för informationsteknologi, Uppsala universitet. Min forskning fokuserar på formell verifiering av komplexa datorsystem, särskilt samtidiga och distribuerade program, och på senare tid även kvantprogram. Jag är särskilt intresserad av att utveckla matematiskt grundade metoder för att resonera om korrekthet i moderna datorsystem.

Innan jag kom till Uppsala var jag postdoktor vid Max Planck Institute for Software Systems i Tyskland, där jag arbetade tillsammans med Rupak Majumdar och Georg Zetzsche med teoretiskt motiverade metoder för verifiering av samtidiga program, ofta inspirerade av praktiska utmaningar i verkliga system.

Jag tog min doktorsexamen i matematisk logik vid Institute of Mathematical Sciences (IMSc) i Indien under handledning av professor R. Ramanujam. Mitt arbete ligger i gränslandet mellan logik, programmeringsspråk och system, med målet att göra rigorösa verifieringstekniker tillämpliga på nya beräkningsparadigm såsom kvantdatorer.

Jag är särskilt intresserad av att arbeta med studenter som tycker om att kombinera teoretiska grunder med problem som uppstår i verkliga datorsystem.

En lista över mina publikationer finns på DBLP [link] och Google Scholar [link].

Forskning

Min forskning fokuserar på formell verifiering av komplexa datorsystem. Jag är särskilt intresserad av metoder för att resonera om korrektheten hos samtidiga och distribuerade program, där verktyg från logik och automatteori spelar en central roll, liksom matematiska metoder mer allmänt. På senare tid har jag även börjat undersöka liknande frågor i samband med kvantprogramvara, där nya beräkningsmodeller och hybrida arkitekturer skapar nya utmaningar för traditionella verifieringstekniker.

Doktorandprojekt: Skalbar verifiering av kvantprogram

Projektet ligger i skärningspunkten mellan formell verifiering, programmeringsspråk och kvantberäkning. I takt med att kvantdatorhårdvara fortsätter att skala upp blir programvarustackarna som styr kvantenheter allt mer avancerade. Moderna kvantprogram involverar ofta hybrida arkitekturer där klassisk styrlogik samverkar nära med kvantkretsar, till exempel vid implementering av kvantfelkorrigering och repeat-until-success-kretsar. Implementeringen av dessa tekniker kräver ofta intermediära mätningar av kvanttillstånd, där mätresultaten används för att styra klassisk kontrollogik. Skalbar och automatiserad verifiering av program med dessa egenskaper ligger bortom kapaciteten hos dagens state-of-the-art-verktyg.

Projektet undersöker skalbara verifieringstekniker för kvantprogram, med fokus på att utveckla matematiskt grundade metoder som kan ge starka garantier om programbeteende samtidigt som de förblir praktiskt användbara för stora system.

Möjliga forskningsinriktningar inom projektet inkluderar:

• utveckling av formella modeller och semantik för hybrida kvant-klassiska program
• anpassning av tekniker från klassisk programverifiering till kvantsammanhanget
• analys av korrekthetsegenskaper hos kvantkretsar och felkorrigerade arkitekturer, både exakt och approximativt
• design av skalbara verifieringsalgoritmer inspirerade av metoder från automatteori
• studier av samspelet mellan symboliskt resonemang och den linjär-algebraiska strukturen hos kvantberäkning

Projektet syftar till att bidra med både teoretiska insikter och mjukvaruverktyg som för forskningsfronten framåt inom verifiering av kvantprogram.

Vem bör söka

Projektet kan vara särskilt intressant för studenter med bakgrund inom teoretisk datavetenskap, programmeringsspråk, formell verifiering eller närliggande områden. Den ideala kandidaten har en stark matematisk bakgrund och tycker om att modellera och analysera komplexa system, kombinerat med ett intresse för att utveckla mjukvaruverktyg som omsätter teoretiska idéer i praktiken. Tidigare erfarenhet av kvantdatorer är meriterande men inte nödvändig.

En bra utgångspunkt för att förstå projektets mål är min POPL-artikel från 2026 “Parameterized Verification of Quantum Circuits” (gemensamt arbete med forskare från Taiwan och Tjeckien), som utvecklar en av de första metoderna för automatisk verifiering av hela familjer av kvantkretsar. arxiv: [link], ACM Digital Library: [link]

Ansökan ska göras via Varbi-portalen [link].