Find Academic Supervisors

Peter MüllerView profile

Professor

• Formal Methods
• Program Verification
• Programming Languages
• +4 more

Prof. Peter Müller is a Full Professor at the Department of Computer Science at ETH Zurich since 2008. Previously, he held positions as Assistant Professor at ETH Zurich (2003-2008), Researcher at Microsoft Research Redmond (2007-2008), and IT project manager at Deutsche Bank. He earned his Diploma in Computer Science from Technical University of Munich (1996) and his Dr. rer. nat. from University of Hagen (2001) with a dissertation on modular verification of object-oriented programs. His research focuses on enabling correct software development through programming languages, verification methods, and tools. Key areas include formal verification for Rust and Go programs (Prusti and Gobra projects), separation logic, security protocols, and distributed systems verification. Müller's work emphasizes practical verification techniques for real-world systems, including secure router implementations and smart contract verification. Recent research trends highlight advancements in hyperproperties, modular reasoning for iterators and closures in Rust, and formal validation of verification tools. His methodologies bridge theoretical foundations with industrial applications, addressing challenges in concurrency, memory safety, and security assurance. Notable contributions include the SCION internet architecture, the Prusti verifier for Rust, and formal verification frameworks for distributed systems. His work often integrates rigorous mathematical foundations with scalable software engineering practices.

Ori LahavView profile

Associate Professor

• Programming Languages
• Verification
• Concurrency
• +4 more

Ori Lahav is a faculty member in the School of Computer Science at Tel Aviv University. His research is generously supported by an ERC Starting Grant and an ISF Grant. He actively supervises PhD and MSc students, and seeks highly motivated candidates for postdoc, PhD, and MSc positions in programming language theory, concurrency, and formal methods. Dr. Lahav completed his PhD at Tel Aviv University under the supervision of Arnon Avron. In 2014, he was a postdoctoral researcher at Tel Aviv University hosted by Mooly Sagiv. From 2014 to September 2017, he was a postdoctoral researcher at MPI-SWS in Germany hosted by Viktor Vafeiadis and Derek Dreyer. His primary research areas focus on programming languages and verification, with specialization in concurrency and relaxed memory models. He also has significant interests in proof-theory, semantics of non-classical logics, and automated reasoning. His work bridges theoretical foundations with practical applications in programming language design and implementation. Dr. Lahav's publication record shows a consistent trajectory of high-impact research in top-tier conferences including PLDI, POPL, OOPSLA, and ESOP. His recent work (2023-2025) demonstrates continued leadership in memory models, concurrency semantics, and verification techniques. His research spans both theoretical contributions in denotational semantics and practical tools for verification. Best Paper Award DISC 2024 Best Student Paper Award DISC 2024 Distinguished Artifact Award ESOP 2022 Distinguished Paper Award OOPSLA 2021 Kleene Award for Best Student Paper LICS 2013 Dr. Lahav actively advises students including Yoav Ben Shimon, Yotam Dvir, Amir Karniel, and Roy Margalit (PhD students), Yuval Katsman Ezra (MSc student), and has alumni including Ori Saporta (MSc) and Abhishek Kr Singh (postdoc, now Assistant Professor at IIIT Hyderabad). He has organized significant events including VMCAI 2024 and Dagstuhl Seminars on persistent programming. His teaching portfolio includes courses on Shared Memory Concurrency Semantics, Programming Language Foundations, and Software Foundations in Coq.

David NaumannView profile

Professor

• formal methods
• software security
• relational verification
• +7 more

David Naumann is Professor and Department Chair of Computer Science at Stevens Institute of Technology. His leadership in the department and active research program positions him as a key figure in programming languages and formal methods research. Naumann's research focuses on formal methods and software security, with particular emphasis on relational and hyperproperty verification , fine-grained confidentiality/integrity policies , and program analysis and verification . His work bridges theoretical foundations with practical applications in security-critical systems. He has developed novel program logics and verification techniques that enable precise reasoning about information flow and security properties. His recent publications (2022-2025) reveal a strong trend toward modular relational verification techniques with applications to pointer programs, distributed systems, and concurrent applications. The research spans theoretical foundations (algebraic structures for alignment) to practical tools (WhyRel prototype), demonstrating both depth and breadth in addressing verification challenges. Naumann has served as program committee co-chair for IEEE Computer Security Foundations Symposium (2021-2022) and has been active on committees for POPL, CCS, CSF, ECOOP, and other top venues. His editorial service includes ACM Transactions on Programming Languages and Systems, Formal Aspects of Computing, and Journal of Object Technology. He leads the Cypress research group at Stevens Institute of Technology and has secured significant funding from NSF, Microsoft Research, and Siemens. His mentoring extends to numerous PhD students who have gone on to successful careers in academia and industry.

Gerardo SchneiderView profile

Professor

• Formal Specification and Analysis of Contracts
• Formalization of Privacy Policies
• Model Checking
• +5 more

Gerardo Schneider is a Full Professor in Computer Science at the University of Gothenburg, Sweden, and holds a joint appointment at Chalmers University of Technology. He serves as Head of the Data Science and Artificial Intelligence (DSAI) Division and has previously led the Formal Methods Division and acted as Director of Graduate Studies. University of Gothenburg: 2009–present Chalmers University of Technology: 2009–present Uppsala University: 2002–2003 University of Oslo: 2005–2009 His research focuses on formal methods for software engineering, including contract specification and analysis , privacy policy formalization , model checking , and runtime verification . He works on verification of real-time systems, embedded systems (e.g., smart Java cards), and blockchain-based smart contracts. Key projects include: X-LEGAL (2020–2023): Smart Legal Contracts (Swedish Research Council) PolUser (2016–2019): User-Controlled Privacy Policies (Swedish Research Council) ARVI (2014–2018): Runtime Verification Beyond Monitoring (ICT COST Action) ReMU (2013–2017): Reliable Multilingual Digital Communication (Swedish Research Council) He has supervised numerous PhD and Master’s students in formal methods, blockchain security, and privacy compliance. His tools include SPeeDI (Polygonal Hybrid Systems Verification), CLAN (Contract Normative Conflict Detection), and AnaCon (Controlled Natural Language Analysis).

Benjamin Lucien KaminskiView profile

Professor

• formal verification
• semantics
• probabilistic programs
• +10 more

Benjamin Lucien Kaminski is a Professor at Saarland University and a Lecturer at University College London . He specializes in quantitative aspects of formal program verification , with a focus on probabilistic and quantum programs , incorrectness logic , and non-classical computation models . His research includes semantics , probabilistic program verification , expected runtimes , and explainable verification . He leads the Examination Board for B.Sc. Computer Science (English) and actively mentors PhD, Master’s, and Bachelor’s students in logic and verification. 2025 : A Taxonomy of Hoare-Like Logics (POPL), Partial Incorrectness Logic (TPSA) 2024 : Quantitative Weakest Hyper Pre (OOPSLA), Caesar: A Verifier for Probabilistic Programs (Dafny), Hoare-Like Triples (Incorrectness-track) 2023 : A Deductive Verification Infrastructure (OOPSLA), Lower Bounds (OOPSLA), A Calculus for Amortized Expected Runtimes (POPL) He has received notable awards including the Ackermann Award (2020), Best Paper at LOPSTR 2020 , and EATCS Best Paper Award at ETAPS 2016 . He has also served on program committees for leading conferences like CAV , POPL , and LICS , and reviewed for prestigious journals such as Journal of the ACM and TOCL .

Deepak GargView profile

Researcher

• Programming Languages
• Secure Compilation
• Type Theory
• +7 more

Deepak Garg is a researcher at the Max Planck Institute for Software Systems (MPI-SWS) in Germany. His work primarily focuses on secure compilation , type theory , and formal verification of software systems. Conference Roles: He has served as an author and committee member in premier programming language conferences such as POPL , PLDI , ICFP , and ESOP since 2015. Research Interests include: Secure compilation techniques for hyperproperty preservation. Modal and refined type theories for cost analysis and concurrency. Formal verification of C code and probabilistic programs. Compiler correctness and decentralized multi-language verification. Contributions span foundational research in programming languages, with a focus on security, complexity, and concurrency. His work has been published in tracks like PriSC , OOPSLA , and ESOP , addressing topics such as data-flow back-translation and robust property preservation.

• Runtime Verification
• Formal Methods
• Concurrency Theory
• +7 more

Adrian Francalanza is a Professor in the Department of Computer Science at the Faculty of Information and Communication Technology, University of Malta. His research is centered on formal methods, runtime verification, and concurrency, with a focus on monitorability and distributed systems. His research interests include: Runtime Verification and Monitor Synthesis Session Types and Protocol Safety Concurrency and Actor-Based Systems Branching and Linear-Time Temporal Logics Probabilistic and Decentralized Monitoring Formal Tools for Cyber-Physical and Distributed Systems The recent publications highlight a strong trend in theoretical and practical advances in monitorability, especially for branching-time and probabilistic systems. His work bridges theory with implementation, often resulting in tools like STMonitor and DetectEr. There is a clear emphasis on session types, runtime enforcement, and the verification of communication protocols in real-world systems such as REST APIs and SMTP. Scientific awards include: Distinguished Paper Award at ECOOP 2025 Best Paper Award at DisCoTec 2022 He has been actively involved in advising and organizing major academic events. He served as Program Chair for GandALF 2024 and 2025, FORTE 2024, and VORTEX workshops. He led a three-year project funded by Rannis on Theoretical Foundations for Monitorability in collaboration with Reykjavik University. He has received grants and recognition for developing practical tools such as DetectEr and STMonitor, which support runtime monitoring of Erlang and session-typed systems. He is associated with several research teams and labs, including: Runtime Verification and Monitorability Research Group at University of Malta Collaborators on the DetectEr project Developers of STMonitor and polyLarva tools International collaborators at Reykjavik University and beyond

Elli AnastasiadiView profile

Assistant Professor

• Formal Verification
• Concurrency Theory
• Parallel Programs
• +7 more

Elli Anastasiadi is an Assistant Professor in the Department of Computer Science at Aalborg University, part of the Technical Faculty of IT and Design. She is a member of the DEIS (Distributed, Embedded and Intelligent Systems) research group, which focuses on formal methods, verification, and intelligent systems. Prior to her current role, she was a postdoctoral researcher at Uppsala University and completed her PhD at Reykjavik University. Education: PhD in Computer Science, Reykjavik University (2022) Master’s in Applied Mathematics and Computer Science, NTUA, Greece Her research centers on formal verification of concurrent and parallel systems , with emphasis on runtime verification, process algebra, and logical foundations. She works extensively with hyperproperties, modal logic, and equational reasoning. Her work bridges theoretical computer science with practical verification tools. Recent publications show a strong trend in logic-based verification , particularly in modal and temporal logics, recursion, and monitor synthesis. Her work often involves complexity analysis and axiomatization of logical systems. Scientific Awards: PhD grant from Reykjavik University research fund She has advised no publicly listed students yet and is actively involved in academic service, including co-organizing workshops and being an invited speaker. She collaborates closely with leading researchers in concurrency theory and formal methods. Labs and Teams: Member of the DEIS research group at Aalborg University, contributing to projects on verification, distributed systems, and intelligent decision-making.

Rayna DimitrovaView profile

Assistant Professor

• Verification
• Reactive Systems Synthesis
• Control and Robotics
• +3 more

Rayna Dimitrova is a Tenure-track faculty member at the CISPA Helmholtz Center for Information Security in Saarbrücken, Germany. Previously, she held positions as Lecturer (Assistant Professor) at the University of Sheffield and University of Leicester, and postdoctoral roles at the University of Texas at Austin and the Max Planck Institute for Software Systems. She earned her PhD from Saarland University. Her research focuses on formal methods, including verification and synthesis of reactive systems, applications to control and robotics, quantitative analysis of probabilistic systems, and information-flow security. Key interests include strategic synthesis under partial observability, probabilistic uncertainty, and continuous dynamics, with applications to autonomous systems. She has served in numerous prestigious roles, including PC co-chair for VMCAI 2024, HYPER 2023, and SMT 2018. Her awards include the RS3 Best Paper Award (VMCAI 2012) and nominations for ETAPS (TACAS 2015) and EMSOFT (2014) Best Paper Awards. Her research group includes PhD students Rafael Dewes, Philippe Heim, and Saleh Soudijani. She has taught courses on reactive synthesis, program analysis, and decision procedures at multiple institutions, including the University of Sheffield and TU Kaiserslautern.

• Cyber-Physical Systems
• Hybrid Systems Verification
• Formal Methods
• +3 more

Stefan Alexander Schupp is a researcher affiliated with the Department of Cyber-Physical Systems at Technische Universität Wien (TU Wien). His work focuses on formal verification, hybrid systems, and controller synthesis for cyber-physical systems. Department: Cyber-Physical Systems (E191-01) Research Affiliation: TU Wien Network Lab Research interests include: Hybrid and stochastic system verification Controller synthesis for real-time systems Formal methods in software engineering Design and analysis of safety-critical systems Automated model checking techniques Flowpipe construction for reachability analysis Recent publications highlight collaborations with researchers from multiple institutions, covering topics such as: Hyperproperty verification in distributed systems Metric Temporal Logic (MTL) controller synthesis Adaptive simplex architectures for bounded-liveness properties Stochastic hybrid automata analysis tools HyPro verification tool developments Probabilistic reachability optimization

• Formal Methods
• Cyber-Physical Systems
• Probabilistic Programming
• +4 more

Ezio Bartocci is a Full Professor in Formal Methods for Cyber-Physical Systems Engineering at TU Wien's Faculty of Computer Science. He leads the Trustworthy Cyber-Physical Systems (TrustCPS) Group within the Cyber-Physical System Research Unit. His research focuses on formal verification, probabilistic systems, and runtime monitoring, with applications in autonomous systems, safety-critical software, and embedded systems. Roles & Affiliations: Full Professor, TU Wien (100% research focus) Principal Investigator in projects funded by EU, WWTF, FFG, and industry partners Chair of the Curriculum Commission for Computer Engineering Editor-in-Chief of the Formal Methods in Outer Space series Research Interests: Formal methods for CPS: verification, synthesis, and runtime monitoring Probabilistic programming and loop analysis Temporal logic specifications and mining Automated tools for safety-critical systems (e.g., Polar, MoonLight) Applications in healthcare, robotics, and autonomous vehicles Key Projects: ProbInG (2020–2025): Analyzing probabilistic loops ARTIST (2021–2026): AI and robotics safety EdgeAI (2022–2025): Optimizing embedded processing TAIGER (2023–2027): Trustworthy AI and CPS Grants & Funding: €10M+ secured from EU Horizon 2020, WWTF, FFG, and industry partners like TTTech Auto AG. Academic Leadership: Teaches courses on logical methods, CPS engineering, and scientific research at TU Wien. Supervises PhD students in formal methods and CPS domains. Tools Developed: Polar (probabilistic loop analyzer), MoonLight (spatio-temporal monitoring), and FIM (fault injection tool).

Derek DreyerView profile

Professor

• Programming Languages
• Type Theory
• Separation Logic
• +6 more

Derek Dreyer is the Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) and an Adjunct Professor in the Saarland Informatics Campus of Saarland University . His research focuses on programming languages , type theory , and formal verification of software systems. Education : PhD in Computer Science from Carnegie Mellon University (2005), advised by Bob Harper and Karl Crary. Key Contributions : Pioneering work in separation logic , ownership types , and memory safety for languages like Rust and C. Awards & Grants : Recipient of significant grants for research on logical foundations of safe systems programming . Leadership : Program Chair for POPL and PLDI, Organizer of RTFM (Red-Hot Topics in Faculty Mentoring), and active role in mentoring students through PLMW. Labs & Teams : Leads a dynamic research group at MPI-SWS , driving collaborative projects in programming languages and systems verification.

Emanuele D’OsualdoView profile

Professor

• Formal Methods
• Programming Languages
• Verification
• +6 more

Emanuele D’Osualdo is a Tenure-track Professor of Formal Methods for Software Engineering at the University of Konstanz. Previously, he held postdoctoral positions at MPI-SWS Saarbrücken (2020-2024) under Derek Dreyer and at Imperial College London (2015-2020) as a Marie Curie Fellow under Prof. P. Gardner. His research focuses on formal methods for software verification, including static analysis, model checking, and compositional verification techniques for concurrent and probabilistic systems. Research interests span Programming Languages, Verification, Security, Concurrency Theory, and Probabilistic Programming. Notable contributions include the Soter tool for Erlang verification, the James Bound library for π-calculus analysis, and foundational work on hierarchical communication topologies. His 2016 doctoral thesis on concurrency verification earned the CPHC/BCS Distinguished Dissertation Award. Recent work includes Bluebell (POPL 2025), advancing probabilistic reasoning via relational lifting, and compositional approaches to hypersafety (OOPSLA 2022). Active in academic service, he has delivered keynotes at HYPER’25 and participates in major conferences like CAV and POPL. Awards: 2016 CPHC/BCS Distinguished Dissertation Award Tools: Soter (Erlang verifier), James Bound (π-calculus library) Grants/Advising: Supervises graduate students at University of Konstanz (details forthcoming) Led the Formal Methods research group focused on concurrency, security, and probabilistic systems at the University of Konstanz.

Martin ZimmermannView profile

Associate Professor

• Temporal Logics
• Reactive Synthesis
• Automata Theory
• +3 more

Martin Zimmermann is an Associate Professor in the Department of Computer Science at Aalborg University, where he leads the Distributed, Embedded and Intelligent Systems research group. Previously, he held roles as a lecturer at the University of Liverpool and postdoctoral researcher at Saarland University and the University of Warsaw. He earned his PhD from RWTH Aachen University, with a Fulbright-funded period at DePaul University in Chicago. Education: PhD in Computer Science, RWTH Aachen University MSc in Computer Science, RWTH Aachen University (with Fulbright at DePaul University) Research Interests: Zimmermann focuses on temporal logics, reactive synthesis, and automata theory, particularly exploring HyperLTL, model-checking techniques, and formal verification challenges. His work bridges theoretical foundations with practical applications in real-time systems and neural-network control. Key Contributions: Notable publications include advancements in HyperQPTL model-checking, complexity analysis of second-order HyperLTL, and robust temporal logics. His research often addresses decidability, computational complexity, and algorithmic solutions for infinite games and reactive systems. Teaching: Teaches courses like Computability and Complexity, Algorithms and Computability, and Computer Architecture at Aalborg University. Service: Served on PCs of major conferences (e.g., CONCUR, CSL) and organized events like MOVEP 2022. Awards: Received the Best Paper Award at MFCS 2021 for groundbreaking work on pushdown automata expressiveness.

Danny Bøgsted PoulsenView profile

Associate Professor

• Formal Methods
• Model Checking
• Cyber-Physical Systems
• +3 more

Danny Bøgsted Poulsen is an Associate Professor at the Department of Computer Science, Aalborg University, affiliated with The Technical Faculty of IT and Design. His research focuses on formal methods, model checking, and cyber-physical systems with applications in security analysis and programming languages. He contributes to projects like BEO-COVID (2020–2020) and IDEA4CPS (2011–2015), which explore decision support tools and foundational cyber-physical systems. His academic background includes advanced work in formal verification and statistical model checking. Key research interests include: Formal methods for string constraints and SMT solvers Statistical analysis of security-critical systems Modelling protocols like DTLS and attack-defense scenarios Applications of formal methods in education and public health Recent work highlights include developing SMTQuery for benchmark analysis, statistical evaluation of bit-flip vulnerabilities, and leveraging large language models for educational feedback. His research outputs span over 36 publications across journals and conferences, with active contributions to UPPAAL tool development and open datasets for reproducibility. Poulsen collaborates internationally on projects involving formal verification of embedded systems and cybersecurity protocols. His work bridges theoretical computer science with practical applications in safety-critical systems.