Find Academic Supervisors

Professor Marta Zofia Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College at the University of Oxford, where she has held a faculty position since 2007. She previously served as Professor of Computer Science at the University of Birmingham (2001–2007), Reader and Lecturer at the University of Birmingham (1994–2001), and Lecturer at the University of Leicester (1986–1994). Her academic career began as Assistant Professor at the Jagiellonian University in Kraków, Poland (1980–1988). Education: BSc/MSc in Computer Science, Jagiellonian University, Kraków MA, University of Oxford PhD, University of Leicester Research Interests: Professor Kwiatkowska spearheaded the development of probabilistic and quantitative verification methods on the international stage. Her work bridges theory and practice through the PRISM model checker—the leading software tool in probabilistic model checking—used worldwide for research and teaching. Application domains include communication and security protocols , nanotechnology designs , power management , ubiquitous computing and systems biology . She investigates automated verification , temporal logics , semantic models for concurrency , real-time systems , and biological process modelling . Current grant funding exceeds £3.7 million from EPSRC, EU and ERC, including the prestigious ERC Advanced Grant VERIWARE. Scientific Awards & Honours: Fellow of the Royal Society Fellow of the ACM Fellow of the European Association for Theoretical Computer Science (EATCS) Fellow of the British Computer Society (BCS) Fellow of the Polish Society of Arts & Sciences Abroad ERC Advanced Grant VERIWARE (€2.046 M, 2010–2015) Top Cited Article Award, Theoretical Computer Science (2005–2010) Best Paper Award, QEST 2006 Doctoral Supervision & Grants: Professor Kwiatkowska actively supervises doctoral students (D.Phil. at Oxford) and post-doctoral researchers. She welcomes applications in areas aligned with her research interests, detailed here . Current students include Charlie Griffin, Daqian Shao, Matthew Yuan and Minghao Liu; past students and researchers number over twenty, many now in faculty or industry leadership roles. Laboratory & Teams: She leads the Oxford Quantitative Verification group within the Department of Computer Science. Ongoing projects include FUN2MODEL, ELSA, FAIR and the flagship PRISM probabilistic model checker. The group maintains strong collaborations with biological, robotics and engineering teams worldwide.

• Automated verification
• Probabilistic model checking
• Temporal logics
• +3 more

Dr. Min Chi is a Professor in the Department of Computer Science at North Carolina State University, where she joined in 2013 as a Chancellor's Faculty Excellence Program cluster hire in the Digital Transformation of Education. Her academic journey includes a Ph.D. and M.S. in Intelligent Systems from the University of Pittsburgh and a B.E. in Information Science and Technology from Xi'an Jiaotong University, China. She completed postdoctoral fellowships at Carnegie Mellon University's Machine Learning Department and Stanford University's Human Sciences and Technologies Advanced Research Institute. Dr. Chi's research focuses on the development and empirical evaluation of cutting-edge Artificial Intelligence, Deep Learning, and Reinforcement Learning frameworks tailored for addressing human-centric challenges. Her work spans multiple domains including advanced learning technologies, AI and intelligent agents, data sciences and analytics, and human-computer interaction. She has made significant contributions to intelligent tutoring systems, healthcare applications, nuclear power systems, and humanitarian efforts such as food distribution and disaster relief. Her publication record demonstrates a strong focus on applying AI techniques to real-world educational challenges, with recent work examining metacognitive knowledge transfer, reinforcement learning for pedagogical policy induction, and deep learning approaches for proactive help in educational settings. Her research also extends to healthcare applications, food distribution systems, and other socially impactful domains. 10 Best Paper, Best Student Paper, and Outstanding Paper Awards Prestigious Alcoa Foundation Engineering Research Achievement Award NSF CAREER Award Dr. Chi leads multiple significant research projects funded by the National Science Foundation, National Institutes of Health, and the Department of Energy, with a total funding exceeding $7 million. Her work bridges theoretical advances in AI with practical applications that address critical societal challenges in education, healthcare, and humanitarian operations.

• Artificial Intelligence
• Deep Learning
• Reinforcement Learning
• +5 more

Mingsheng Ying is a Distinguished Professor and Research Director of the Centre for Quantum Computation and Intelligent Systems (QCIS) at the Faculty of Engineering and Information Technology, University of Technology Sydney, Australia. He also holds the position of Cheung Kong Professor at the State Key Laboratory of Intelligent Technology and Systems, Department of Computer Science and Technology, Tsinghua University, Beijing, China. Professor Ying graduated from the Department of Mathematics, Fuzhou Teachers College, Jiangxi, China, in 1981. His primary research interests span quantum computation (particularly quantum programming and model-checking quantum systems), programming theory and formal methods, and the foundations of artificial intelligence (focusing on logic and uncertainty). As an author of the books "Foundations of Quantum Programming" (Elsevier - Morgan Kaufmann 2016) and "Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs" (Springer-Verlag, 2001), he has published over 100 papers in top international journals and conferences. His recent research publications demonstrate a strong focus on quantum programming languages, verification techniques for quantum systems, and the theoretical foundations of quantum computation. The trend in his work shows increasing emphasis on formal verification methods for quantum systems, particularly model-checking techniques for quantum Markov chains and quantum processes. His research bridges theoretical computer science with quantum information theory, creating frameworks for reliable quantum software development. Editorial Board, Artificial Intelligence, Elsevier, Amsterdam Editorial Board, Fuzzy Sets and Systems, Elsevier, Amsterdam Vice President, International Fuzzy Systems Association (elected in 2005) Program Chair, IFSA 2005, World Congress of International Fuzzy Systems Association Chairman, Chinese Association of Fuzzy Systems and Mathematics Professor Ying has secured significant research funding including multiple Australian Research Council Discovery Projects such as "Model-checking quantum Markov chains: towards verification techniques for quantum cryptographic systems" (2013-2015) and "Process algebra approach to distributed quantum computation and secure quantum communication" (2011-2013). His work has also received funding from the National Natural Science Foundation of China and Tsinghua University. At QCIS, he leads research in quantum software theory and methodology, with applications in quantum cryptography and secure communication.

• Quantum Computation
• Quantum Programming
• Model-checking Quantum Systems
• +5 more

Aniello Murano is a Professor of Computer Science at the Department of Electrical Engineering and Information Technologies , University of Naples Federico II. He serves as Scientific Director of the ASTREA (Automated Strategic Reasoning) Laboratory and leads cutting-edge research in Artificial Intelligence, Strategic Reasoning, Multi-Agent Systems , and Formal Verification . Research Interests : Strategic reasoning under perfect/imperfect information, specification/verification/synthesis of reactive systems, temporal/modal logics, automata theory, parity games, game theory, mechanism design, and formal languages. Notable Projects : PNRR Research Unit Coordinator (2023-2025) on Resilient AI, PRIN 2020 Unit Coordinator (RIPER: Resilient AI-Based Self-Programming and Strategic Reasoning), H2020-MSCA SEAL (Principal Coordinator). Awards & Honors : JPMorgan Faculty Research Award (2022), Royal Society Award (2016), Best Paper PRIMA (2015), INDAM Project Leader (2023), Italian Scientific Habilitation (2017-2018). Students & Postdocs : Supervised 6 PhD students (e.g., Silvia Stranieri, Vadim Malvone) and mentored postdocs such as Munyque Mittelmann and Bastien Maubert. Laboratory : Leads ASTREA Lab, focusing on automated strategic reasoning and resilient AI systems.

• Artificial Intelligence
• Strategic Reasoning in Multi-Agent Systems
• Formal Verification
• +6 more

David Parker is Professor of Computer Science at the University of Oxford and a Tutorial Fellow at Trinity College. His research focuses on formal verification methods for checking system correctness, particularly quantitative verification techniques for probabilistic systems. As leader of the PRISM and PRISM-games projects, he develops tools for analyzing safety, reliability, and performance properties in complex systems. Current research explores verification of AI systems, robust decision-making under uncertainty, and multi-agent systems using stochastic games. His work bridges theoretical foundations with applications in autonomous systems, robotics, and healthcare technology. Recent publications demonstrate advancements in probabilistic temporal logic, robust policy learning, and bisimulation techniques for Markov models. These works consistently emphasize formal guarantees for safety-critical applications and novel approaches to model checking. ETAPS Test-of-Time Tool Award (2024) HVC Award (2016) Professor Parker mentors PhD students in verification, control synthesis, and AI safety, with research funded by ERC, EPSRC, and industrial partners. He serves on editorial boards for Formal Aspects of Computing and ACM Transactions on Autonomous Systems.

• Formal Verification
• Probabilistic Model Checking
• Quantitative Analysis
• +2 more

Linan Chen is an Associate Professor in the Department of Mathematics and Statistics at McGill University since 2014, following a postdoctoral position at the same institution (2011–2014). He holds a Ph.D. from MIT (2011, supervised by Daniel Stroock) and a B.Sc. from Tsinghua University (2006). His research focuses on probability theory and its intersections with analysis and geometry, including partial differential equations, functional analysis, Gaussian measures, and random geometry. He is affiliated with the Probability Lab of the Centre de Recherches Mathématiques (CRM) and the CNRS-Unite Mixte Internationale (CNRS-UMI) since 2014. Chen teaches advanced probability courses such as Honours Probability (Math 356) and Advanced Probability Theory I/II (Math 587/589), alongside special topics courses like Topics in Geometry and Topology (Math 599). He has advised students including Leila Sloman, Reinhold Willcox, Ulysse Blau, and Olivier Nadeau-Chamard through independent study programs. His research explores cutting-edge topics in probability, including Gaussian free fields, degenerate diffusion equations, and asymptotic properties of geometric stochastic structures. Recent work addresses high-dimensional phenomena, stochastic processes in geometry, and applications in mathematical physics. Chen’s contributions span theoretical advancements and methodological innovations, with publications in journals such as the Journal of Theoretical Probability, Annales Henri Poincaré, and SIAM Journal on Mathematical Analysis.

• Probability Theory
• Analysis
• Geometry
• +4 more

Ana Sokolova is a Professor in the Department of Computer Science at the University of Salzburg. She is affiliated with the Faculty of Digital and Analytical Sciences and actively contributes to research in theoretical computer science. University: University of Salzburg Faculty: Faculty of Digital and Analytical Sciences Department: Computer Science Email: ana.sokolova@plus.ac.at Her research focuses on probabilistic systems , concurrency theory , convex algebras , and formal verification . This work bridges theoretical foundations with practical applications in distributed computing and programming semantics. Recent publications highlight advancements in trace semantics , determinization , probabilistic anonymity , and coalgebraic modeling . Key trends include the integration of Markov chains , nondeterministic systems , and algebraic structures for formal verification.

• Computer Science
• Theoretical Computer Science
• Formal Methods
• +3 more

Egor Kostylev serves as an Associate Professor in the Department of Informatics within the Faculty of Mathematics and Natural Sciences at the University of Oslo. His research focuses on the theoretical foundations connecting symbolic and sub-symbolic artificial intelligence, particularly examining relationships between formal logic systems and machine learning approaches. His educational background includes an MSc (Specialist, 2005) and PhD (Candidate, 2009) from Lomonosov Moscow State University under Prof. Vladimir A. Zakharov. He subsequently held research positions at the University of Edinburgh (2010-2013) and the University of Oxford (2013-2020) before joining the University of Oslo in 2020. Kostylev's research interests center on bridging symbolic AI formalisms with sub-symbolic approaches. He investigates connections between various logics (Description Logics, Temporal Logics, Datalog), query languages (SPARQL, Regular Path Queries, OTTR), and machine learning formalisms (Graph Neural Networks, Markov Logic Networks). His work addresses critical challenges in Explainable, Trustworthy, and Green AI through theoretical foundations that connect different AI paradigms. His publication record demonstrates consistent high-impact contributions in theoretical computer science and AI, with numerous publications in top venues including AAAI, LICS, Journal of the ACM, and ICLR. His recent work shows a clear trajectory toward unifying logical reasoning with neural network approaches, particularly through graph neural networks and their connections to logical formalisms. The research spans theoretical foundations of knowledge representation, temporal reasoning in knowledge bases, and the logical expressiveness of modern neural architectures. As a research leader, Kostylev supervises multiple PhD students including Shuwen (Aurora) Liu, Maximilian Pflüger, Roxana Pop, Dongzhuoran Zhou, and Erik Snilsberg. He serves as a Research Theme Leader for the Integreat SFF: Norwegian Centre for Knowledge-driven Machine Learning. His teaching responsibilities include IN3020/4020 Database Systems courses. He leads the Data and Knowledge Management (DKM) research group at the University of Oslo, which focuses on foundational aspects of knowledge representation, database theory, and the intersection with modern machine learning techniques. The group actively collaborates with international researchers and contributes to advancing theoretical understanding of how symbolic and neural approaches to AI can complement each other.

• Foundations of AI
• Symbolic AI
• Description Logics
• +9 more

Abbas Edalat is a Professor of Computer Science and Mathematics at Imperial College London, and an Adjunct Professor at the Institute for Research in Fundamental Sciences, Tehran. He leads two research groups: Algorithmic Human Development and Continuous Data-Types and Exact Computation. His work spans computational mathematics, psychotherapy models, and exact real-number computation. Notably, he received the LICS 2017 Test-of-Time Award for foundational contributions to logic in computer science. Research interests include self-attachment psychotherapy, computational differential calculus, topology, and bisimulation in probabilistic systems. He has pioneered exact computation frameworks for real numbers, geometry, and dynamical systems, with applications in neuroscience and artificial intelligence. Professional activities include keynote talks at conferences like IJCNN and workshops on psychotherapy in Iran and the UK. Teaching includes advanced courses on dynamical systems, quantum computing, and computational techniques. He advises PhD students globally and chairs initiatives like the Science and Arts Foundation to expand educational access in developing nations. His interdisciplinary work bridges mathematics, computer science, and clinical psychology.

• Computer Science
• Mathematics
• Exact Computation
• +7 more

Sylvain Lombardy is a Professor at the University of Bordeaux, affiliated with the Laboratoire Bordelais de Recherche en Informatique (LaBRI) and the Enseirb-Matmeca engineering school within the Institut Polytechnique de Bordeaux. His research focuses on automata theory, formal languages, and theoretical computer science, particularly in weighted automata, formal methods, and algebraic properties of automata. He leads the Formal Methods research team at LaBRI and contributes to projects like the Awali and Vaucanson software platforms for automata manipulation. Education: PhD in Computer Science (2001, ENST Paris), Habilitation à Diriger des Recherches (2005, University of Paris Diderot). His work bridges theoretical foundations with practical tools, emphasizing algorithmic and algebraic aspects of automata. Notable contributions include studies on automata minimization, determinization, and the interplay between rational expressions and automata constructions. Research Interests: Automata Theory, Formal Power Series, Weighted Automata, Tropical Semirings, Algebraic Automata Theory, and Computational Models for Discrete Systems. His recent work explores two-way automata, Hadamard series, and applications in formal verification. Publications highlight contributions to the structure and properties of automata, with a focus on formal methods and algorithmic decidability. Key works address unambiguity, determinism, and the minimization of weighted automata across various semirings. Collaborations include projects on automata-based kernels for machine learning and XML formats for automata descriptions. He has developed influential software tools such as Awali (finite-state machine platform) and Vaucanson (automata manipulation framework), demonstrating practical applications of theoretical research. His work is supported by grants exploring automata in computational linguistics and discrete mathematics.

• Automata Theory
• Formal Languages
• Theoretical Computer Science
• +3 more

Joost-Pieter Katoen is a full Professor at RWTH Aachen University and Head of its Computer Science Department since 2012. He also holds a part-time (20%) Professorship at the University of Twente . His research focuses on model checking , probabilistic verification , formal semantics , and software verification , with applications in aerospace systems. His work has led to significant tools like MRMC (probabilistic model checker), COMPASS (AADL analysis tool-set), and libalf (learning automata library). He has authored over 18 international projects (total €5.2 million) and graduated 12 PhD students. Scientific Awards : Member, German National Academy of Sciences (Leopoldina), 2024 ACM Fellow, 2020 ERC Advanced Grant, 2018 Honorary doctorate, Aalborg University, 2017 Teaching Award, RWTH Aachen, 2010 Philips Early Career Development Award, 1988 Research Trends (from articles): His recent work spans probabilistic program verification , quantitative game theory , Markov chain analysis , and parameter synthesis for stochastic systems, with applications in AI, quantum computing, and fault tree analysis. Leadership & Service : Katoen co-founded the QEST conference , chairs ETAPS steering committee, and has led numerous program committees (CONCUR, TACAS, QEST). He has served on editorial boards and organized conferences/seminars globally.

• Model Checking
• Formal Verification
• Probabilistic Models
• +5 more

Dr. Kirsten Winter is an Honorary Senior Fellow at the University of Queensland's School of Electrical Engineering and Computer Science. Her research focuses on formal verification, concurrent programming, and weak memory models. She has contributed significantly to areas such as model checking, railway interlocking systems, and behavior trees. Her work spans theoretical foundations (e.g., linearizability, concurrency semantics) and practical applications in security and embedded systems. Recent projects include the Program Analysis Cell and BASIL: Boogie Analysis for Secure Information-Flow Logics. Winter has collaborated extensively with researchers like Graeme Smith and Robert Colvin. Her most recent publications address speculative execution vulnerabilities and compositional reasoning in weak memory architectures.

• Formal Verification
• Concurrent Programming
• Computer Security
• +3 more

Ramavarapu S Sreenivas is a Professor in the Industrial and Enterprise Systems Engineering department at the University of Illinois at Urbana-Champaign , with research appointments at the Coordinated Science Laboratory (CSL) and the Information Trust Institute (ITI ). He holds a joint affiliation with the Electrical and Computer Engineering department and serves as the Arthur Davis Faculty Scholar since 2016. Ph.D. , Electrical and Computer Engineering, Carnegie Mellon University (1990) M.S.E.E. , Carnegie Mellon University (1987) B.Tech , Electrical Engineering, Indian Institute of Technology Madras (1985) His research focuses on Discrete-Event/Discrete-State (DEDS) systems , applying Coding Theory, Machine Learning, and Information Theory to develop near-optimal supervisory policies for applications in wireless networks, automated manufacturing, and healthcare systems . He leads the Center for Autonomous Construction and Manufacturing at Scale (CACMS) , established in 2023. Recent publications highlight advancements in liveness enforcement in Petri nets , fault-tolerant control , and IoT-based load scheduling . His work bridges theoretical rigor with practical implementations in Distributed Control, Network Coding , and Reinforcement Learning . UIUC Campus Award for Excellence in Graduate and Professional Teaching (2023) Arthur Davis Faculty Scholar (2016) Senior Member, IEEE (2002) James Franklin Sharp Outstanding Teaching Award in Industrial Engineering (2017, 2012) Sreenivas has taught graduate and undergraduate courses in Control Systems, Integer Programming, and Financial Computing since 1992. He co-instructed courses in Health Technology and contributed to the Master of Science in Financial Engineering (MSFE) program, which ranks 4th nationally.

• Discrete-event systems
• Control theory
• Petri net modeling
• +6 more

Peter Buneman is a prominent academic affiliated with the University of Edinburgh, UK. His research primarily focuses on databases, data provenance, XML, and semistructured data. He has held significant roles in advancing computational models for data citation, provenance tracking, and distributed systems. Key areas of expertise include database systems, graph algorithms, and collaborative data curation platforms. Buneman's work integrates theoretical foundations with practical applications in pharmacology data, digital libraries, and scientific data management. His contributions to data provenance and citation systems have shaped standards in academic and industrial settings. Notable projects include the Database Wiki platform for collaborative data management and the MITra framework for graph traversal. Buneman collaborates extensively with co-authors like Susan Davidson, Wenfei Fan, and Val Tannen. Publications span 1974–2025, emphasizing methodologies for data integration, distributed computing, and computational biology. His work bridges theoretical computer science with real-world applications in biomedicine and information systems.

• Databases
• Data Provenance
• XML
• +5 more

Prof. Martin Otto is a Professor of Mathematics at the Technische Universität Darmstadt, specializing in Logic and Mathematical Foundations of Computer Science. He holds a position in the Department of Mathematics (Fachbereich 4) and serves as Dean of Studies. His academic journey includes a PhD from the University of Freiburg (1990), habilitation from RWTH Aachen (1996), and prior roles as a Lecturer/Reader at Swansea University (1999–2003). Research Interests: Mathematical Logic, Model Theory, Complexity Theory, Algorithmic Model Theory, Finite Model Theory, and Logic in Computer Science. Notable contributions include work on bisimulation, guarded logics, and inquisitive semantics. His research bridges structural properties in mathematics and computational expressiveness. Teaching: Courses span Mathematical Logic, Model Theory, Linear Algebra, and Modal Logics. Recent offerings include Introduction to Mathematical Logic (2024/25), Logic & Knowledge Representation, and advanced seminars on model-theoretic topics. Publications: Over 50 peer-reviewed papers in journals like the Journal of Symbolic Logic, and conference proceedings such as LICS and CSL. Key works address guarded fragments, bisimulation invariance, and finite model theory applications. Affiliations: Member of the Logic Group at TU Darmstadt. Editorships include the Bulletin of Symbolic Logic and Lecture Notes in Logic. Organized workshops like AlMoTh 2020 (cancelled due to pandemic) and participated in Simons Institute programs (2016).

• Mathematical Logic
• Model Theory
• Complexity Theory
• +4 more