Find Academic Supervisors

• Embedded Systems
• Synchronous Languages
• Theorem Proving
• +8 more

Timothy Bourke is a Researcher at Inria in the PARKAS team , affiliated with the Informatics Department of École normale supérieure (ENS) . He also serves as an Adjunct Professor at the Informatics Department of École Polytechnique , contributing to both institutions' academic and research missions. Research Focus: His work centers on rigorous approaches to modeling, programming, and verifying embedded control systems. This includes developing and analyzing Vélus (Verified Lustre) and Zélus (synchrony + ODEs) , integrating formal methods with practical applications like robotic wheelchair control systems, infrared sensors, microkernel operating systems, microprinter components, and wireless routing protocols. Academic Service: Active in program committees for conferences including DAC , ECRTS , EMSOFT , iFM , JFLA , and SETTA , including chairs/co-chairs at ESOFT 2019 , JFLA 2022-2023 , and SETTA 2024 . Regular reviewer for journals like ACM Transactions on Embedded Computing Systems and Real-Time Systems . Students: Advised Guillaume Baudart (2013–2017), Lélio Brun (2016–2020), Paul Jeanmaire (2020–2024), and Basile Pesin (2020–2023). Labs/Teams: Core member of the PARKAS team at Inria, focusing on embedded systems and synchronous language design. His technical contributions include software tools like Muttlight , Sundials/ML , and Urpal for timed trace inclusion testing. He also teaches courses such as L3 at ENS , MPRI INF559 , and CSE205 at École Polytechnique .

Wolfgang J. PaulView profile

Professor

• Hardware design
• Computer architecture
• Formal verification of processors and microkernels

Wolfgang J. Paul is a Professor of Informatics at Saarland University in Saarbrücken, Germany, holding this position since 1986. He previously served as Dean of the Faculty of Technology from 1998 to 2000. His academic career includes a Research Staff Member role at IBM Research Laboratory in San Jose (1982-1986), a professorship in Mathematics at Bielefeld University (1976-1982), and a postdoctoral position at Cornell University (1974-1976). His research focuses on Hardware design, Computer architecture, and Formal verification of processors and microkernels, with emphasis on mathematically rigorous validation of critical computing components. This work bridges theoretical computer science and practical hardware implementation, contributing to system reliability and security through formal methods. His major recognitions include: Member of Academia Europaea (2006) Leibniz-Preis (1987) IBM Invention Achievement Award (1986) Professor Paul has held significant leadership roles including Dean of the Faculty of Technology and maintains active research in formal verification methodologies, influencing both academic and industrial approaches to hardware correctness.

Gernot HeiserView profile

Professor

• Operating Systems
• Microkernels
• Cybersecurity
• +8 more

Scientia Professor Gernot Heiser is a leading researcher in trustworthy computing systems at the University of New South Wales, where he holds the John Lions Chair of Operating Systems. He is the founder and leader of the Trustworthy Systems Research Group, recognized globally for applying formal methods to ensure security and safety of real-world computing systems. His work spans operating systems, cybersecurity, and dependable systems. Professor Heiser completed his academic qualifications with a BSc in Physics from Freiburg in 1982, an MSc in Physics from Brock in 1984, and a PhD in Computer Engineering from ETH Zurich in 1991. He has been an academic at UNSW since completing his PhD and became a full professor in 2002. He was awarded the title of Scientia Professor in 2011, UNSW's highest academic honor. His research focuses on fundamental solutions to cybersecurity challenges through trustworthy systems. Key areas include microkernels and microkernel-based systems, highly-secure and dependable systems, high-assurance systems, analysis and prevention of cyber threats, real-time systems, virtualization, embedded and cyberphysical systems, and architectural support for operating systems. Professor Heiser's work has resulted in practical applications, most notably the seL4 microkernel, which is the world's first operating-system kernel with a proof of implementation correctness and security enforcement. Notable awards include: Fellow, Engineers Australia (2022) Member of the German Academy of Sciences Leopoldina (2022) ACM Software System Award (2022) ACM SIGOPS Hall of Fame Award (2019) Fellow of the IEEE (2016) Fellow of the ACM (2014) Professor Heiser actively supervises honours, MPhil, and PhD students in his research areas, with projects typically requiring strong backgrounds in operating-system internals or formal methods. He has co-founded Open Kernel Labs in 2006, leading to the L4-embedded microkernel being deployed on billions of mobile devices, including the secure enclave of iOS devices. His research group, the Trustworthy Systems group, was created in 2003 at NICTA and has been wholly at UNSW since 2021.

RobbyView profile

Professor

• Formal Methods
• Software Engineering
• Programming Languages
• +3 more

Robby is a Professor in the Department of Computer Science at Kansas State University's College of Engineering, holding the Don and Linda Glaser - Carl and Mary Ice Keystone Research Scholar title. He maintains an active research profile through the SAnToS Lab and has been continuously affiliated with the university since 2004. His educational background includes: Ph.D. in Computer Science from Kansas State University (2004) M.S. in Computer Science from Kansas State University (2000) B.S. in Computer Science from Oklahoma State University (1998) Robby's research centers on formal methods and software engineering , specializing in specification and verification techniques for high-assurance systems. His work develops user-friendly formal languages and cost-efficient verification algorithms that significantly enhance software trustworthiness in safety-critical domains like aerospace and defense systems. This research bridges theoretical foundations with practical industrial applications through tools like the Sireum framework. His publication record (2021-2025) reveals a strong trajectory toward integrated verification ecosystems, particularly the Sireum suite (Logika, Slang) and HAMR toolset for AADL-based development. These works consistently address model-code verification gaps and contract-based testing in cyber-physical systems, demonstrating growing industry adoption through collaborations with organizations like Galois and NASA. Notable recognitions include: NASA Turning Goals into Reality award (2003) NSF CAREER award (2007) ICSE Most Influential Paper award (2000) ACM SIGSOFT Impact award (2010) FMICS Best Tool Paper Award (2024) Robby's research program combines significant funding from sources like the NSF CAREER grant with active industry partnerships. His SAnToS Lab serves as a hub for developing verification methodologies that scale from academic prototypes to real-world deployment in safety-critical systems, emphasizing practical toolchains for assurance engineering. He leads the SAnToS Lab (Software Analysis and Test Organization), which focuses on advancing formal verification techniques for high-integrity software through frameworks like Sireum and HAMR, with applications spanning microkernels, cyber-physical systems, and educational tools.

Olaf SpinczykView profile

Professor

• Embedded Systems
• Aspect-Oriented Programming
• Operating Systems
• +3 more

Olaf Spinczyk is a Professor in the Department of Computer Science 12 at Technische Universität Dortmund, leading the Embedded System Software Group. Previously, he held positions at Friedrich-Alexander-Universität Erlangen-Nürnberg and the University of Magdeburg. His research focuses on embedded systems, aspect-oriented programming, and operating system design. Affiliations: Technische Universität Dortmund: Head of Embedded System Software Group Former roles: University of Erlangen-Nürnberg (Dept. of Computer Science 4) and Magdeburg University Research Interests Spinczyk specializes in tailor-made operating systems , embedded systems , and aspect-oriented programming . His work emphasizes software product lines for embedded environments, fault tolerance, and energy-efficient system design. Key projects include: CiAO: Aspect-oriented OS product line AspectC++: AOP extension for C++ FAME-DBMS: Database management system family FAIL*: Fault-injection framework Recent Work Recent research explores energy-aware device drivers, cyber-physical system reliability, and virtualization strategies for industrial applications. He has contributed to frameworks like vGridLab for smart grid testing and PhyNetLab for IoT-based warehouses. Awards & Activities No explicit awards listed, but notable contributions include leadership roles in EuroSys and conference organization (e.g., PLOS workshops, AOSD tutorials). Active in academic service, including program committees for AOSD and MMB. Labs & Teams Leads the Embedded System Software Group at TU Dortmund, collaborating on projects involving automotive systems, real-time computing, and cloud federation strategies.

Gunnar TeegeView profile

Professor

• Formal Verification
• Virtualization
• Distributed Systems
• +7 more

Prof. Dr. Gunnar Teege is a faculty member at the Institute for Computer Engineering within the Faculty of Computer Science at Bundeswehr University Munich. His career spans over two decades, focusing on distributed systems, virtualization, and formal verification of operating system components. He has led numerous research projects, including collaborations with institutions like the Runder Tisch GIS eV and the Bavarian State Office for Surveying and Geoinformation. Education: Diploma in Computer Science from Technical University of Munich (1985), Doctorate in Computer Science from TUM (1991) Affiliations: Member of GI (Gesellschaft für Informatik) and ACM (Association for Computing Machinery) Research interests include formal verification of software components for secure systems, virtualization frameworks, distributed systems, military communications, geospatial data interoperability via OpenGIS standards, computer-supported cooperative work (CSCW), and E-Learning platforms. His work often bridges theoretical and applied domains, particularly in defense IT systems and education technology. He has contributed to projects like Targeteam (XML-based adaptable teaching materials), HoBIT (high-security embedded systems), and MiKscHA (microkernel applications for high-security environments). His publications emphasize modularity, tailorability, and security in software design. Teaching activities at Bundeswehr University Munich include courses on operating systems, distributed systems, virtualization, and cybersecurity. Previously, he taught problem-based learning in computer science at TU Munich and developed virtual lectures for the Virtual University of Bavaria (vhb) from 2001–2005.

Mark P JonesView profile

Professor

• Programming Language Design
• Programming Language Implementation
• Low-Level Systems Programming
• +6 more

Mark P Jones is a Professor and Chair of the Maseeh College of Engineering & Computer Science at Portland State University . He holds a B.A. (Hons, first-class) in Mathematics and an M.Sc. and D.Phil. in Computation from the University of Oxford. His research spans programming language design, implementation, and application, with a focus on advanced language technologies for low-level systems programming and expressive type systems for secure, reliable software. He is best known for designing the Hugs interpreter and Gofer systems, which have been foundational in functional programming education. His work includes the NSF-funded CEMLaBS project (Award CNS-1422979) exploring language-based security via microkernels like seL4 and pork. Selected Courses: CS 410/510 Languages and Low-Level Programming CS 320 Principles of Programming Languages CS 457/557 Functional Programming Scientific Awards: Winner, British Computer Society Competition for Distinguished Dissertations in Computer Science (1993) He maintains the LLP Labs GitHub repository and has contributed to tools like mil-tools for systems programming education.

Paul WolfgangView profile

Professor

• Hardware design
• Computer architecture
• Formal verification of processors and microkernels

Paul Wolfgang is a Professor at Saarland University since 1986, previously serving as Dean of the Faculty of Technology from 1998 to 2000. His academic career includes roles as a Research Staff Member at IBM's San Jose Research Lab (1982–1986) and as a Wissenschaftlicher Rat und Professor for Mathematics at Bielefeld University (1976–1982). He completed his postdoctoral studies at Cornell University (1974–1976). Education details include a Postdoctoral fellowship at Cornell University from 1974 to 1976. Prior to that, he held academic positions at Bielefeld University and IBM's research division. His research focuses on Hardware design, Computer architecture, and Formal verification of processors and microkernels. These areas emphasize advancing computational efficiency and ensuring reliability through rigorous validation methods. Notable recognitions include the Leibniz-Preis in 1987, the IBM Invention Achievement Award in 1986, and election as a Member of Academia Europaea in 2006. Paul Wolfgang has contributed significantly to academic leadership and research, though specific details regarding grants or advisees are not documented in the provided materials.

Jim Alves-FossView profile

Professor

• Cybersecurity
• Formal Verification
• Operating Systems
• +2 more

Jim Alves-Foss is a University Distinguished Professor of Computer Science at University of Idaho's College of Engineering, specializing in high-assurance computing systems and cybersecurity. Core research domains: Formal methods for security verification Operating system security architectures Critical infrastructure protection Automated security policy enforcement Publications demonstrate consistent focus on: Rigorous verification of security properties (e.g., seL4 kernel) Development of automated analysis tools (fuzzing, SDN policy) Industrial control system protection frameworks Adversary-aware risk assessment methodologies

Francesco Zappa NardelliView profile

Associate Professor

• Formal Verification
• Programming Languages
• Type Systems
• +3 more

Francesco Zappa Nardelli is a part-time Associate Professor at École Polytechnique and a Research Scientist at Meta. He is currently on leave from Inria Paris, focusing on formal verification and programming language design. Member of the POPL'23 Program Committee Presented key research on formal verification of microkernel IPC and Julia subtyping algorithms Research Focus: His work bridges formal methods, programming language theory, and systems software. Recent efforts include compiler optimization, type system innovation, and safety-critical systems verification. Scientific Recognition: Recognized as an invited speaker at DeepSpec and ENTROPY workshops, with publications in top venues like CPP, OOPSLA, and ECOOP.

Peter W. O'HearnView profile

Professor

• Programming Languages
• Formal Verification
• Separation Logic
• +5 more

Peter W. O'Hearn is a Professor of Computer Science at University College London and a Research Scientist at Meta AI (FAIR). He has held academic positions at Syracuse University, Queen Mary University of London, and University College London, before joining Facebook (now Meta) in 2013 as part of the acquisition of the verification startup Monoidics. His career spans over 25 years of research in programming languages and logic, with significant contributions to both theoretical foundations and practical industrial applications. O'Hearn's research primarily focuses on formal reasoning about programs, with his most notable contributions being the co-invention (with John Reynolds) of Separation Logic and the development of Incorrectness Logic. His work bridges the gap between theoretical computer science and practical software engineering, emphasizing how fundamental theory, tool development, and real-world application can mutually reinforce each other. He has consistently advocated for the integration of formal methods into industrial software development practices. His research has led to the development of the Infer program analyzer, which runs internally on Meta's code bases and has detected over 100,000 bugs that have been fixed by developers. Infer is also used in production at other major companies including Amazon, Mozilla, Spotify, and Marks and Spencer. His recent work on Incorrectness Logic represents a paradigm shift from traditional program verification approaches, focusing on bug finding rather than correctness proving. O'Hearn has received numerous prestigious awards recognizing both his theoretical contributions and practical impact: Fellow of the Royal Society (elected 2018) Fellow of the Royal Academy of Engineering (2016) 2016 Gödel Prize 2016 CAV Award Two POPL MIP awards Honorary doctorate from Dalhousie University (2018) 2021 IEEE Cybersecurity Award for Practice Throughout his career, O'Hearn has successfully translated theoretical advances into practical tools used at scale in industry. His work on Separation Logic led directly to Infer, while his more recent work on Incorrectness Logic aims to provide foundations for next-generation bug catching tools. He has maintained a strong academic presence while working in industry, continuing his professorship at UCL alongside his role at Meta. O'Hearn leads research efforts at the intersection of formal methods and practical software engineering at Meta, focusing on scaling static analysis techniques to handle the massive codebases typical of modern technology companies. His work has significantly influenced how large tech companies approach software verification and bug detection.

• Operating Systems
• Distributed Systems
• Computer Networks
• +3 more

Andrew Tanenbaum is a Professor Emeritus at Vrije Universiteit Amsterdam, affiliated with the Faculty of Science's Computer Systems department. He holds a PhD in Physics from the University of California and a Bachelor's in Physics from MIT. His expertise spans operating systems, distributed systems, and computer networks, with a focus on fault tolerance and system security. Tanenbaum has authored seminal textbooks like 'Operating Systems: Design and Implementation' and 'Computer Networks.' He has been awarded the Eurosys Lifetime Achievement Award (2015), ACM Fellowship (1996), IEEE Fellowship (1998), and honorary doctorates (2008, 2011). His research emphasizes reliable system design, including projects like MINIX, and explores fault injection, storage systems, and live updating mechanisms. Tanenbaum has supervised 20 PhD theses and contributed to over 300 publications. His work bridges theoretical foundations with practical implementations, influencing modern operating system and network architecture.

Yohannes BekeleView profile

Assistant Professor

• Cyber-physical System Security
• Reliable Computing
• Edge Computing
• +5 more

Dr. Yohannes Bekele is an Assistant Professor of Electrical and Computer Engineering at Hampton University's School of Engineering, Architecture and Aviation. His research focuses on cyber-physical system security, reliable distributed computing, and edge computing. He holds a Ph.D. from North Carolina A&T State University (2023), MSc from Addis Ababa University (2018), and BSc from Arba Minch University (2007). Prior to academia, he worked as a senior engineer/project manager at Ethio Telecom and held technical roles in various organizations. His expertise includes hardware fault analysis, secure embedded systems, and transportation IoT security. He currently teaches courses aligned with his research and leads projects on cyber-physical system reliability. Dr. Bekele is affiliated with professional organizations like NSBE and IEEE. Recent publications highlight work on federated learning-based intrusion detection systems, QEMU fault injection tools, and rowhammer attacks on embedded devices. His research bridges theoretical cybersecurity concepts with practical implementation in edge and embedded systems. Dr. Bekele has no listed scientific awards but demonstrates active participation in conferences such as IEEE HOST and AFRICON. His teaching and research emphasize hands-on projects, reflected in courses taught and industry collaborations.

Marc FeeleyView profile

Professor

• Dynamic programming languages
• Functional programming languages
• Programming language design and implementation
• +4 more

Marc Feeley is a Full Professor at Université de Montréal's Department of Computer Science and Operations Research (DIRO), part of the Faculty of Arts and Sciences. He leads research in programming languages, compilers, and runtime systems. His work focuses on dynamic languages like Scheme and JavaScript, emphasizing efficient implementation, compiler optimization, and parallel processing. Education details are not explicitly listed, but his academic career includes a PhD in Computer Science (Brandeis University, 1993) and a Master's in Computer Science from Université de Montréal (1986). His research spans over 30 years with projects funded by CRSNG and FQRNT grants. Research interests include: Dynamic and functional programming languages Compiler optimization techniques Parallel computing architectures Runtime systems and garbage collection Language implementation for embedded systems Recent work focuses on: Small, efficient Scheme implementations (e.g., Gambit) Optimizing Python and JavaScript compilers Self-hosting transpilers for resource-constrained environments Key publications include foundational work on garbage collection algorithms, compiler optimizations for dynamic languages, and embedded system implementations. He has advised over 30 graduate students since 1996. Awards include a best paper award at IFL'09 and sustained research funding from major Canadian grants. His Gambit Scheme compiler remains a widely used open-source project.

• Formal Methods
• Functional Programming
• Unifying Theories of Programming (UTP)
• +7 more

Dr. Andrew Butterfield is a faculty member at the School of Computer Science and Statistics, Trinity College Dublin. He serves as Head of the Foundations and Methods Group and actively contributes to Lero: the Irish Software Research Centre. His research focuses on Formal Methods and Functional Programming, particularly the Unifying Theories of Programming (UTP) paradigm, with applications in clinical pathways, medical device software, and spacecraft operating systems. Current research includes developing UTP theories for shared-variable concurrency, rely/guarantee reasoning, and separation logic in collaboration with Jim Woodcock. He also explores Process Modelling Language (PML) semantics with John Noll and Anila Mjeda. His contributions feature proof-assistance tools like UTP2 Theorem Prover, UTP Calculator, and ReasonEq implemented in Haskell. Andrew leads funded projects such as ESA's RTEMS-SMP (2019) and SFI's FMHIDA (2016-2020). Past projects encompass formal verification of separation kernels, Handel-C language semantics, and NAND flash memory models. He has taught courses in Formal Methods, Functional Programming, and Concurrency, while serving on editorial and program committees including Formal Aspects of Computing.