Ramanathan Thinniyam Srinivasan

Short presentation

I am an Assistant Professor at Uppsala University working on program verification, concurrency, and quantum computing. I am currently recruiting a PhD student on scalable verification of quantum programs, combining techniques from programming languages, logic and formal verification.

Keywords

• program verification
• quantum computing
• concurrency
• model checking
• programming languages.

Biography

I am an Assistant Professor (tenure track) in the Division of Computer Systems at the Department of Information Technology, Uppsala University. My research focuses on the formal verification of complex computing systems, particularly concurrent and distributed programs, and more recently quantum programs. I am broadly interested in developing mathematically grounded techniques that help reason about correctness in modern computing systems.

Before joining Uppsala, I was a postdoctoral researcher at the Max Planck Institute for Software Systems in Germany, where I worked with Rupak Majumdar and Georg Zetzsche on theoretically motivated approaches to the verification of concurrent programs, often inspired by practical challenges in real systems.

I received my PhD in Mathematical Logic from the Institute of Mathematical Sciences (IMSc), India, under the supervision of Prof. R. Ramanujam. My work sits at the intersection of logic, programming languages, and systems, with the goal of making rigorous verification techniques applicable to emerging computing paradigms such as quantum computing.

I am particularly interested in working with students who enjoy combining theoretical foundations with problems arising in real computing systems.

A list of my publications can be found on DBLP [link] and Google Scholar [link].

Research

My research focuses on the formal verification of complex computing systems. I am particularly interested in techniques for reasoning about the correctness of concurrent and distributed programs, using tools from logic and automata theory in particular, and mathematics in general. More recently, I have begun exploring similar questions in the context of quantum software, where new computational models and hybrid architectures pose challenges for traditional verification techniques.

PhD project: Scalable Verification of Quantum Programs

The project lies at the intersection of formal verification, programming languages, and quantum computing. As quantum hardware continues to scale, the software stacks used to control quantum devices are becoming increasingly sophisticated. Modern quantum programs often involve hybrid architectures in which classical control logic interacts closely with quantum circuits, for example in the implementation of quantum error correction and repeat-until-success circuits. Implementing these techniques often requires intermediate measurements of quantum states, with the measurement outcomes used to drive classical control logic. Scalable and automated verification of programs with these features is beyond the capabilities of the current state-of-the-art tools.

This project investigates scalable verification techniques for quantum programs, with a focus on developing mathematically grounded methods that can provide strong guarantees about program behavior while remaining practical for large systems.

Possible directions of the project include:

• developing formal models and semantics for hybrid quantum-classical programs
• adapting techniques from classical program verification to the quantum setting
• reasoning about correctness properties of quantum circuits and error-corrected architectures, both exactly and approximately
• designing scalable verification algorithms inspired by techniques from automata theory
• exploring the interaction between symbolic reasoning and the linear-algebraic structure of quantum computation

The project aims to contribute both theoretical insights and software artifacts, advancing the state of the art in quantum program verification.

Who should apply

The project may be of interest to students with a background in theoretical computer science, programming languages, formal verification, or related areas. The ideal candidate has a strong mathematical background and enjoys modelling and analysing complex systems, together with an interest in developing software tools that put theoretical ideas into practice. Prior experience with quantum computing is helpful but not required.

A useful starting point for understanding the goals of the project is my POPL 2026 paper “Parameterized Verification of Quantum Circuits” (joint work with collaborators from Taiwan and Czechia), which develops one of the first methods for automated verification of entire families of quantum circuits. arxiv: [link], ACM Digital Library: [link]

The application should be made via the Varbi portal [link].