Find Academic Supervisors

Arnd HartmannsView profile

Associate Professor

• Stochastic Timed Systems
• Hybrid Systems
• Probabilistic Model Checking
• +5 more

Arnd Hartmanns is an associate professor in the Formal Methods and Tools group at the University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS). Previously, he was a postdoc at both the University of Twente and Saarland University's Dependable Systems and Software group, where he also completed his Ph.D. in computer science in 2015. He has led multiple research projects including the NWO VIDI project 'Trustworthy Analysis of Stochastic Timed Systems (TruSTy)', the Interreg North Sea project 'STORM_SAFE', and coordinates the MSCA RISE project 'MISSION'. His primary research interests focus on modeling tools and formalisms for stochastic timed and hybrid systems, particularly the Modest framework. Hartmanns has been a strong advocate for reproducibility in Computer Science research through artifact evaluation initiatives, tool competitions like QComp, and standardized benchmark sets. His work bridges theoretical foundations with practical applications across various domains including network-on-chip systems, power grids, and space communication infrastructure. He has made significant contributions to probabilistic model checking, statistical verification techniques, and formal methods for system analysis. Hartmanns serves on numerous program committees, particularly focusing on artifact evaluation for conferences like TACAS, QEST, and FORMATS. His leadership in establishing reproducibility standards has influenced the formal methods community significantly. The trends in his recent publications show a strong emphasis on verified implementations of verification algorithms, statistical model checking techniques that go beyond standard approaches, and applications of formal methods to increasingly complex real-world systems. Scientific Recognition 2016 Best Dissertation Award by the GI/ITG Technical Committee for 'Measurement, Modelling and Evaluation of Computing Systems' Hartmanns has supervised numerous Master's and PhD students through his research projects, though specific names aren't listed in the provided information. His grant portfolio includes several major projects funded by NWO (VENI, VIDI, Open Competition) and European programs (MSCA RISE, Interreg North Sea). He is actively involved in developing educational materials for formal methods and has contributed to establishing benchmark sets that are now standard in the field. His work on the Modest modeling language and toolset has created an important infrastructure for quantitative verification research. The integration of formal verification with machine learning techniques, particularly in strategy learning and decision tree generation, represents one of his more recent research directions that connects formal methods with emerging AI approaches.

Stavros TripakisView profile

Associate Professor

• Formal Methods
• Computer-Aided Verification and Synthesis
• Safety-Critical Systems
• +4 more

Stavros Tripakis is an Associate Professor at the Khoury College of Computer Sciences at Northeastern University , where he joined in 2018. He is on sabbatical during the 2024-2025 academic year. His research focuses on the foundations of software and system design , emphasizing formal methods , computer-aided verification and synthesis, with applications to safety-critical, embedded, and cyber-physical systems, security, and trustworthy AI. He leads a group developing theory and tools for designing better systems. Recent publications explore distributed protocol synthesis, neural network verification, and inductive invariant inference, reflecting trends in formal methods for AI and distributed systems. His work often intersects with automated reasoning, model checking, and tool development. Scientific awards include the Distinguished Artifact Award at TACAS 2018 for the Refinement Calculus of Reactive Systems (RCRS) toolset. He advises Derek Egolf , Daniel Melcer , and William Schultz (graduated 2025). Former postdocs include Rômulo Meira-Góes (now Penn State) and Eunsuk Kang (now CMU). Current projects include the NSF FMitF grant (2023-2027) on safe multi-agent reinforcement learning and the NSF SaTC grant (2018-2022) on protocol design.

• Programming Languages
• Static Analysis
• Software Engineering
• +7 more

Qirun Zhang is the Catherine M. and James E. Allchin Early Career Associate Professor in the School of Computer Science at Georgia Institute of Technology. He earned his Ph.D. in Computer Science and Engineering from The Chinese University of Hong Kong (2013) and bachelor's degree in Computer Science from Zhejiang University (2009). Zhang teaches graduate courses in compilers, software analysis, and program analysis, including CS 6340 Software Analysis and Test (Fall 2024) and CS 4240 Compilers and Interpreters (Spring 2025). His research focuses on improving software reliability and security through program analysis and compiler optimization techniques. Key research areas include computational complexity, analytic combinatorics, graph theory, and formal languages. Current projects include SLOT (SMT-LLVM Optimizing Translation) , Mutual Refinements of Context-Free Language Reachability , and Context-Free Language Reachability with Transitive Redundancy Elimination , among others. Zhang's research has produced award-winning work including the SIGSOFT Distinguished Paper Award (FSE 2023) and PLDI Distinguished Paper Award (2020). He has advised multiple students including Ph.D. graduates Shuo Ding (2024) and Yuanbo Li (now at Facebook), with Benjamin Mikek and Camille Bossut currently pursuing their Ph.D.s. As an academic leader, Zhang has served as: Artifacts Chair: PLDI'26, PLDI'25 Program Committee: PLDI'26, POPL'26, SAS'25, ASPLOS'25, SAS'24, FSE'24 External Reviewer: PLDI'19, PLDI'18 His group maintains active GitHub repositories for tools like Perses (syntax-guided program reduction) and Skeletal Program Enumeration (compiler testing framework). Zhang also contributes to educational resources by maintaining course materials on static analysis, symbolic execution, and webassembly analysis.

• Programming Languages
• Reversible Computing
• Software Systems
• +2 more

Robert Glück is a Professor at the Department of Computer Science under the Faculty of Science , University of Copenhagen. He also served as a Visiting Professor at the National Institute of Informatics, Tokyo . His research spans programming languages , reversible computing , and metaprogramming , with a focus on energy-efficient computation. Email: glueck@di.ku.dk Phone: +45 29611655 Address: Universitetsparken 5, Building B, 2100 Copenhagen Ø Glück's research interests center on reversible computing , program generation , and metaprogramming , particularly for low-energy systems. His work includes developing reversible logic circuits, invertible interpreters, and tools for program inversion via term rewriting systems. Recent publications highlight advancements in reversible flowchart languages , partial evaluation techniques , and compiler design . Key themes include garbage-free reversibility, memory-efficient algorithms, and formal verification of reversible systems. Scientific Awards: Japan Society for the Promotion of Science (JSPS) Fellowship Grants & Projects: Presto Basic Research Grant (JST) Danish Council for Strategic Research (DSF) project Danish Council for Independent Research (FNU) project Administrative Roles: Current member of the Study Board for Mathematics and Computer Science Former Head of Studies for the Master in Computer Science Professional Activities: IFIP Technical Committee WG 2.11 member (2004–) Steering Committee roles at LOPSTR 2024, FLOPS 2024, HCVS 2024, RC 2024 Editorial Board member for New Generation Computing (2005–)

James R. WilcoxView profile

Assistant Professor

• Programming Languages
• Computer Science
• Formal Methods
• +5 more

James R. Wilcox is an Assistant Professor of Computer Science at the University of Washington , where he teaches courses like Introduction to Programming , Foundations of Computing , and Operating Systems . His research focuses on programming languages , formal methods , and distributed systems verification . PhD, University of Washington BS, Williams College (2013) Wilcox's research bridges software engineering and formal verification , with applications to distributed systems, concurrent programming, and tools like mypyvy for verification. He has published extensively in top venues such as POPL , PLDI , and CAV , emphasizing compositional techniques and proof assistants like Coq. He has received two Distinguished Paper Awards (PLDI 2015, PLDI 2020) and contributes to frameworks like Verdi for verifying distributed systems. Outside academia, he is a baritone in Seattle's choral ensembles and an avid long-distance cyclist.

Sebastien PillementView profile

Lecturer

• Computer Engineering
• Embedded Systems
• Computer Architecture
• +3 more

Sébastien Pillement is a Lecturer at Polytech'Nantes, the College of Engineering of the University of Nantes, and a member of the ASIC research team within the IETR UMR 6164 laboratory. His career spans over 13 years at the IUT of Lannion (University of Rennes 1) before joining the University of Nantes in 2012. He holds a PhD in Computer Science from the University of Montpellier II (1998) and a Habilitation à Diriger des Recherches (HDR) from the University of Rennes 1 (2010). Current Research Focus: Dynamically Reconfigurable Architectures (DRA), Hardware Security, Fault-Tolerant Embedded Systems, NoC (Network-on-Chip), Design Methodologies. Teaching Areas: Digital Circuits, Computer Architecture, Operating Systems, Real-Time Systems, and Algorithms for Embedded Computing. His research explores flexible and efficient architectures for embedded systems, emphasizing real-time management, reliability, and security. Key article trends include RISC-V processors, neural network acceleration on MPSoC, formal verification of arithmetic circuits, and runtime FPGA scheduling. Collaborations span international institutions like the University of Toronto and CEA, as well as industrial partners such as STMicroelectronics and Thales. PhD Students : Current: Laureline Dubucq (Security & AI), Mustafa Ibrahim (Ultra-Low Power AI), Téo Biton (Runtime Anomaly Detection), Mohamed Amine Zhiri (Adaptive NoC), Juliette Pottier (RISC-V Protection). Graduates: Quentin Dariol (Neural Network Timing), Alexis Duhamel (FPGA Scheduling), Safouane Noubir (Security in Multi-Core Systems), Hai Dang Vu (Probabilistic Timing Analysis), David Pallier (Sensor Clock Synchronization). Projects : Current: ADAPTING (2023-2029), FITNESS (2023-2027), SEC-V (2022-2025), NOP (2021-2025). Past: SPARTE (2015-2018), ARDyT (2011-2015), FosFor (2008-2011).

Giovanni SilenoView profile

Lecturer

• Artificial Intelligence
• Logic Programming
• Knowledge Representation
• +5 more

Giovanni Sileno is an academic specializing in Artificial Intelligence, Logic Programming, and Knowledge Representation, with teaching appointments at the University of Amsterdam, EPITA Paris, and Université Pierre et Marie Curie. His primary affiliation is with the Informatics Institute at the University of Amsterdam where he serves as a Lecturer. His research interests span multiple domains within computer science, focusing particularly on formal methods for normative systems, agent-based programming, and logic-based knowledge representation. His work bridges theoretical computer science with practical applications in policy modeling, forensic science, and business information systems. Dr. Sileno has developed several notable software projects including AgentScriptCC for single-threaded intentional agents, DCPLschema for normative policy specifications, and libraries for normative primitives in Answer Set Programming. His GitHub activity shows consistent contributions from 2012 through 2025, indicating active engagement in both research and development. His publications reflect a strong focus on formal methods applied to practical problems, with particular emphasis on normative systems, agent architectures, and logic programming applications. The research trajectory shows evolution from foundational topics in logic and numeral systems toward increasingly sophisticated applications in policy modeling and agent-based systems. As an educator, he has taught across multiple institutions and disciplines, covering topics from basic programming paradigms to advanced knowledge representation and formal modeling techniques. His teaching spans undergraduate to master's level courses in information studies, cognitive science, data science, and forensic science.

• Algorithms
• Theory & Logic
• Programming Languages & Verification
• +4 more

Faraz Ghahremani is a researcher affiliated with the Max Planck Institute for Software Systems (MPI-SWS), part of the Max Planck Society. His work focuses on foundational and applied research in computer science, with a strong emphasis on algorithmic theory, programming languages, and system security. He contributes to interdisciplinary areas such as cyber-physical systems and distributed systems, addressing challenges in networked and mobile environments. His research interests span a broad spectrum, including formal verification, privacy-preserving technologies, and the intersection of social systems with computational methods. While specific publications or grants are not detailed in the provided text, his affiliation with MPI-SWS—a leading research institution—suggests involvement in cutting-edge projects at the forefront of computer science. No specific academic awards, supervised students, or detailed grants are explicitly mentioned in the available information. For further details, direct inquiry to MPI-SWS or his official profile would be required.

• Functional Programming
• Software Testing
• Formal Methods
• +3 more

John Hughes is a Professor at Chalmers University of Technology. His research focuses on functional programming, software testing, and formal methods. He is a co-author of the Haskell programming language and a pioneer of QuickCheck, a property-based testing tool. His work bridges foundational theory with practical applications in software engineering. Research Interests: Development of functional programming paradigms and their applications Property-based testing and automated software validation Type systems and compiler optimization techniques Concurrency and parallelism in functional languages His publications span influential works like Why Functional Programming Matters (1989) and A History of Haskell (2007). He has contributed to open-source tools and frameworks widely used in academia and industry.

William HallahanView profile

Assistant Professor

• Formal methods
• Functional languages
• Network systems
• +3 more

William Hallahan is an Assistant Professor in the School of Computing at Binghamton University. He joined the faculty in August 2022 following his PhD in Computer Science from Yale University (May 2022), where he was advised by Ruzica Piskac. His research focuses on formal methods, functional languages, and network systems, with an emphasis on techniques that simplify code verification and automated reasoning. Education: PhD in Computer Science, Yale University, 2022 BA in Mathematics and Computer Science, College of the Holy Cross Research interests include: Program verification for functional languages Automated debugging and repair systems Network system verification (firewalls, P4 programs) Control plane synthesis for programmable networks Publications highlight contributions to symbolic execution, firewall repair, and P4 verification frameworks. Current research emphasizes developing practical formal techniques to reduce programmer error and improve code reliability. He maintains an active research group with multiple funded PhD positions available starting Spring 2023.

Michael FosterView profile

Researcher

• Software Testing
• Causal Inference
• Model Inference
• +3 more

Dr. Michael Foster is a Researcher and Research Software Engineer at the School of Computer Science, University of Sheffield. He specializes in software testing methodologies, causal inference, and formal methods for system modeling. His work focuses on developing tools for automated model inference, particularly Extended Finite State Machines (EFSMs), and applying causal reasoning to improve software testing. Education: PhD in Computer Science (2017-2020) from the University of Sheffield, supervised by Prof. John Derrick and Dr. Achim Brucker. His doctoral research addressed EFSM inference from black-box software execution traces, integrating genetic programming and formal verification techniques. Research Projects: Principal contributor to the CITCoM project, applying causal inference to computational model testing. Developed the causal testing framework and EFSM inference tool, which formalizes model merging and data dependency analysis. Explored metamorphic testing, automated verification of trace properties, and active learning techniques for EFSMs. Key Contributions: Published extensively on causal testing, EFSM inference, and algorithmic testing strategies. His work bridges formal methods with practical software engineering challenges, emphasizing automated tools and rigorous validation frameworks.

• Access Control
• Cloud Security
• Critical Infrastructure Protection
• +3 more

Dr Antonios Gouglidis is a Senior Lecturer in the Department of Computing and Communications at Lancaster University, specializing in theoretical and applied security. His research focuses on designing secure systems through the integration of theoretical informatics and practical industry experience. His research interests span several critical areas in cybersecurity including access control models and policies , Cloud security , Critical Infrastructure Protection (CIP) , and formal verification through model checking. His work bridges theoretical security concepts with practical implementation challenges. Analysis of his recent publications (2022-2025) reveals a strong focus on emerging security challenges in cloud environments, 5G networks, and operational technology. His research demonstrates particular expertise in multi-layer threat analysis, security-vs-QoS optimization, and formal verification techniques. He frequently applies game theory approaches to security problems and has increasingly incorporated AI/ML techniques into his security frameworks. Dr Gouglidis has supervised PhD students including Ovini Gunasekera and Igor Ivkic. His research has been supported by significant projects such as: SL:H2020 SANCUS (2020-2023) BEIS: Nuclear Research and Development Programme (2019-2022) Enable Ancillary Services bY Renewable Energy Sources (2018-2021) Towards Ultimate Convergence of All Networks (2017-present) Resilient communication services protecting end-user applications (2016-2020) His work has practical applications in critical infrastructure protection, particularly in energy sector systems and industrial control environments. Dr Gouglidis maintains an active research profile with consistent publication output across top security venues.

Thomas LembergerView profile

Researcher

• Software Verification
• Formal Methods
• Software Testing
• +9 more

Thomas Lemberger is a researcher in the Department of Computer Science at Ludwig-Maximilians-Universität München (LMU Munich), contributing to the Software and Computational Systems Lab. He specializes in software verification, formal methods, and automated testing, with a focus on improving tool efficiency and scalability. His work includes extensions to CPAchecker, such as distributed summary synthesis and cooperative verification approaches, as well as developing user-friendly tools like CoVeriTeam GUI. His research interests involve integrating verification into build systems and IDEs, optimizing verification workflows, and exploring hybrid techniques that combine testing and formal methods. He has actively participated in competitions like SV-COMP and Test-Comp, contributing tools like PRTest and Nacpa. His projects aim to reduce tool restarts, enhance fault localization, and streamline verification processes through parallel portfolio analyses. Thomas mentors students on topics related to verification tool development, test-case generation, and open-source software. His contributions are supported by grants from the DFG (CONVEY, COOP, IDEFIX), emphasizing cooperative verification and scalable analysis. Recent work focuses on enabling developers to use verification tools seamlessly within their existing workflows.

Philipp WendlerView profile

Lecturer

• Software Verification
• Formal Methods
• Program Analysis
• +5 more

Philipp Wendler is an academic lecturer in the Department of Computer Science at Ludwig-Maximilians-Universität München (LMU Munich). He is affiliated with the Software and Computational Systems Lab and actively involved in research, teaching, and open-source tool development. As an employee representative in the steering committee of the Institute of Informatics, he contributes to institutional governance. His research focuses on software verification, formal methods, and program analysis. Key projects include CPAchecker (a configurable verification framework) and BenchExec (a benchmarking tool). His work emphasizes practical applications in automated testing, energy-efficient algorithms, and reproducible benchmarking. Publications span topics like interpolation-based model checking, energy measurement tools, and strategies for software verification competitions. He has contributed to advancing predicate analysis, k-induction, and refinement selection techniques. Notable achievements include leading the development of CPAchecker and BenchExec, which are widely used in academic and industrial verification efforts. His research addresses challenges in scalable verification, flaky test analysis, and energy-aware computing.

Maximilian R. OdenbrettView profile

Researcher

• Formal Methods
• Parallel Computing
• Model Checking
• +3 more

Maximilian R. Odenbrett was a PhD student at Eindhoven University of Technology (2010–2011), collaborating with RWTH Aachen University's MOVES group. His research focused on Efficient Multi-Core Model Checking , leveraging NVIDIA's CUDA for parallel processing on GPGPUs. He specialized in formal methods, stochastic model checking, and parallel programming for multi-core systems. Education : Diplom-Informatiker (Computer Science) from RWTH Aachen University (2004–2010), with a minor in Psychology. Research Interests : Development of parallel algorithms for formal verification, application of GPUs in bioinformatics (e.g., biological network analysis), and model-based analysis of software systems. His work bridges theoretical formal methods with practical parallel computing solutions. Publications : Focused on applying GPGPUs to model checking and bioinformatics problems, as seen in his BMC Bioinformatics paper (2012) and conference contributions on AADL specification analysis (2010). His research emphasizes scalability and efficiency in computational systems. Affiliations : Collaborated with Prof. Joost-Pieter Katoen's MOVES group at RWTH and Prof. P.A.J. Hilbers' BMI group at TU Eindhoven. His work contributed to the EMCMC project on multi-core model checking.