Stefan Krastanov is an Assistant Professor at the University of Massachusetts Amherst, focusing on quantum hardware design, control, and optimization across multiple layers of quantum computing and networking technologies. His work bridges physical hardware descriptions with logical circuit compilation, emphasizing resilience in noisy quantum systems. Research Interests include Quantum Hardware Design, Entanglement-Based Networking, Quantum Error Correction, and Modeling Software for Quantum Systems. His primary lab is the Quantum Information Lab , with affiliations to the Advanced Classical and Quantum Information Research Lab. Recent work trends highlight advancements in quantum repeater networks, error-corrected compilation, and photonic neural networks. His publications span topics like non-Markovian dynamics simulation, NP-hard optimization in quantum dot arrays, and scalable spin quantum memory control. Labs and Teams: Quantum Information Lab (leading experimental/theoretical work) and collaborations through the Advanced Classical and Quantum Information Research Lab.
Elena Grigorescu is a Professor at the University of Waterloo, Department of Computer Science. She holds a Ph.D. from the Massachusetts Institute of Technology (2010), an M.S. from MIT (2006), and a B.A. from Bard College (2004). Her research focuses on sublinear-time algorithms, error-correcting codes, computational complexity, and learning theory. She explores foundational aspects of algorithms with constraints on time/space, privacy-preserving computation, and applications in graph theory and optimization. Her work includes advancements in spanner algorithms for network design, differential privacy in sublinear-time settings, and learning-augmented approaches for online optimization. Recent publications address trace reconstruction, privacy-utility trade-offs, and combinatorial optimization techniques. Grigorescu is actively involved in conferences like APPROX/RANDOM and IEEE Foundations of Computer Science, contributing to algorithmic theory and practical implementations. Her research emphasizes theoretical rigor while addressing real-world challenges in data analysis and distributed systems. No awards or formal advisees are explicitly listed in the provided information.
Bryan Parno is a Professor at Carnegie Mellon University in the Departments of Electrical & Computer Engineering and Computer Science . He is the recipient of the Kavčić-Moura Chair and leads the Secure Foundations Lab , focusing on end-to-end secure systems through formal verification. Research spans secure systems , applied cryptography , distributed systems , and zero-knowledge proofs Developed Verus (verified Rust systems) and Project Everest (verified HTTPS stack) Key contributions include Ironclad , Flicker , and Pinocchio , with impacts on Intel CPUs and Windows/iOS security models His work emphasizes open-source tools and reproducibility , often published in top venues like POPL, PLDI, and IEEE S&P. Recent projects address WebAssembly security and formal verification of complex distributed systems . Major Awards Jay Lepreau Best Paper Award (OSDI 2025) IEEE Cybersecurity Award for Practice (2024) Sloan Research Fellowship (2018) Test-of-Time Awards (IEEE S&P 2023, IEEE S&P 2020) Best Paper Awards at USENIX Security, OOPSLA, and PLDI
John van de Wetering is an Assistant Professor at the Theoretical Computer Science group of the Informatics Institute, University of Amsterdam, working with the QuSoft research center. He co-authored the open-access book Picturing Quantum Software and developed the PyZX quantum compiler. His research spans quantum computation and quantum foundations, focusing on diagrammatic methods like the ZX-calculus and ZH-calculus. Quantum circuit optimization and verification Quantum foundations via algebraic/compositional methods Co-creator of PyZX His recent publications explore multi-qutrit systems, completeness of graphical calculi, and quantum state representations. Supervises students in quantum computing, including Lia Yeh and Sarah Li. Directs the new Master's program in Quantum Computer Science at UvA. Actively contributes to open-source projects and international conferences. Notable collaborations include Aleks Kissinger, Neil J. Ross, and QuSoft researchers. Uses GitHub for DiZX development (qudit extension of PyZX). No explicit scientific awards mentioned.
Timothy M. Jones is a Professor of Computer Architecture and Compilation at the University of Cambridge Computer Laboratory, where he leads research in systems-level computing. He is also a Fellow at Gonville and Caius College, contributing to academic leadership and student mentorship within the collegiate system. His primary affiliation with the Computer Laboratory positions him at the forefront of systems research within the university. Dr. Jones's research focuses on extracting various forms of parallelism (thread-level, data-level, memory-level) to enhance computational performance while addressing energy efficiency and reliability challenges. His work spans compiler design, binary translation, and microarchitecture optimization, with specific interest areas including: Compiler technologies for functional and parallel programming Hardware reliability and fault tolerance mechanisms Binary analysis and instrumentation frameworks Memory system optimization and virtual memory management Security enhancements through binary modification Runtime systems for heterogeneous architectures Analysis of his recent publications reveals strong emphasis on systems-level innovation, particularly in fault tolerance techniques, binary analysis tools, memory optimization, and parallel execution frameworks. His work consistently bridges theoretical computer science with practical hardware implementation challenges. Dr. Jones maintains active participation in the academic community through conference leadership roles, including serving as Program Co-Chair for CGO 2026 and committee positions at premier venues including ISMM, CGO, and ECOOP. He contributes to open-source academic resources through GitHub and maintains professional engagement via Twitter.
Neelakantan R. Krishnaswami is a Professor of Computer Science at the University of Cambridge's Computer Laboratory , and a Fellow of Trinity College . His research focuses on the intersection of program verification, programming language design, and foundational topics like type theory and semantics. His work spans areas such as refinement types, parser design, separation logic for systems software, and the semantics of reactive programming. Notable contributions include the Datafun language for higher-order Datalog and the λert type theory for explicit refinement types. He has also developed foundational frameworks for verifying imperative programs using advanced type systems and logical relations. Key publications include 'Explicit Refinement Types' (ICFP 2023), 'flap: A Deterministic Parser with Fused Lexing' (PLDI 2023), and 'CN: Verifying Systems C Code' (POPL 2023). His work frequently addresses challenges in efficiency, correctness, and modularity for both functional and imperative systems. His awards include Distinguished Paper Awards at PLDI 2019 and POPL 2020. His research integrates theoretical rigor with practical tooling, exemplified by contributions to languages like Coq, Lean, and Haskell.
Benjamin J. Delaware is an Assistant Professor of Computer Science at Purdue University. His research focuses on programming languages, formal verification, and tools for ensuring software correctness using mechanized theorem provers. He holds a Ph.D. from The University of Texas at Austin (2013), an MSc from Washington University in St. Louis (2007), and a B.S. from Truman State University (2005). His work emphasizes practical formal methods, including static enforcement of privacy policies, compiler design for oblivious computation, and automated verification techniques. Key contributions include tools like Taypsi, KestRel, and HACCLE. His research bridges theory and practice, addressing challenges in software security, correctness, and efficiency. Publications span top venues like POPL, PLDI, and OOPSLA, reflecting a strong focus on foundational programming language concepts. Collaborations with researchers like Suresh Jagannathan and Qianchuan Ye drive advancements in automated reasoning and secure computation.
Carlo A. Furia is an Associate Professor at the Software Institute within the Faculty of Informatics at Università della Svizzera italiana (USI). He leads the ATOM research group and is actively involved in advancing formal methods in software engineering. His work bridges theoretical rigor with practical applicability, particularly in verification, automated repair, and empirical analysis of software systems. PhD in Computer Science, Politecnico di Milano Master of Science in Computer Science, University of Illinois at Chicago Laurea in Computer Science and Engineering, Politecnico di Milano His research focuses on making formal methods practical through automation, combining diverse techniques, and conducting thorough empirical evaluations. He is particularly interested in using Bayesian data analysis to assess software engineering data. His work spans program verification (e.g., AutoProof), contract inference, API usability, and multilingual program analysis. His recent publications highlight trends in automated program repair, JVM bytecode analysis, Android security, and empirical methodologies. These works reflect a consistent emphasis on correctness, reliability, and empirical validation in software development. Scientific service includes: Associate Editor, Empirical Software Engineering (EMSE) journal Program Committee member, FM 2026, FormaliSE 2026, ASE 2025, iFM 2025 He has advised students and leads the ATOM group, which develops tools for software analysis. He teaches courses such as Software Analysis, Programming Fundamentals, and Software Design & Modeling. Current research directions include improving empirical evaluation rigor and enhancing verification at lower code levels like bytecode.
Daniel J. Sorin is a Professor of Electrical and Computer Engineering at Duke University's Pratt School of Engineering, where he also serves as Associate Chair of Education. He holds joint appointments in both the Electrical and Computer Engineering department and Computer Science department, and is recognized as a Bass Fellow for his contributions to education and research. His research focuses on computer architecture with specific expertise in memory systems, cache coherence protocols, fault tolerance, and verification-aware design. Dr. Sorin's work bridges theoretical computer architecture with practical implementations, often incorporating coding theory to solve architectural challenges. His research group has made significant contributions to automated protocol generation, hardware acceleration, and robot motion planning systems. Dr. Sorin's publications reveal a consistent focus on memory consistency models, cache coherence protocols, and verification techniques. His recent work has expanded into robot motion planning acceleration, FPGA resource management, and novel error correction techniques for emerging memory technologies. The trend shows increasing interdisciplinary work connecting computer architecture with robotics and machine learning applications. Program Chair of HiPEAC 2017 Co-chair of IEEE Micro's Top Picks selection committee (2016) Lois and John L. Imhoff Distinguished Teaching Award (2011) NSF CAREER Award recipient IEEE Micro Top Pick awards (2011, 2015) ACM Senior Member As an advisor, Dr. Sorin has mentored numerous PhD students who have gone on to successful careers at leading technology companies including Google, Microsoft, Oracle, and Nvidia. His research group maintains strong industry connections and has produced influential work in cache coherence protocols, memory systems, and fault-tolerant architectures. He has also authored the widely-used textbook 'A Primer on Memory Consistency and Cache Coherence' (2nd edition). Dr. Sorin leads an active research laboratory focused on next-generation computer architecture challenges, with ongoing projects in hardware acceleration, memory systems, and robot motion planning. His group collaborates with researchers across multiple disciplines including robotics, coding theory, and semiconductor design.
Dr. John Wickerson is an Associate Professor in the Circuits and Systems group at the Department of Electrical and Electronic Engineering, Imperial College London. His research focuses on improving the reliability of high-performance computing through formal methods, with contributions to high-level synthesis, memory models, and concurrency verification. He holds leadership roles including Course Director for the Electrical and Information Engineering degree and Deputy Tutor for PhD students. Research Interests: Formal Verification of Hardware/Software Systems High-Level Synthesis (HLS) and FPGA Compilation Weak Memory Models and Concurrency Semantics Fuzz Testing for Hardware Tools Compiler Optimization and Correctness Digit Elision and Arbitrary-Precision Arithmetic Notable Achievements: Best Paper Award at EuroSys 2024 (database isolation validation) Pioneered formal methods for HLS tools (e.g., QuteFuzz, C4) Co-developed the C4 C compiler concurrency checker Published over 60 peer-reviewed papers across top venues (ASPLOS, PLDI, FPGA) Lab/Team: Part of the Circuits and Systems group at Imperial College, collaborating with industry partners like Kaihong Yann and ARM.
Manos Kapritsos is an Associate Professor in the Department of Computer Science and Engineering at the University of Michigan's College of Engineering. He leads the GLaDOS research group focusing on reliability of distributed systems through formal verification and fault-tolerant replication techniques. His research spans: Formal verification of concurrent and distributed systems Fault-tolerant replication protocols beyond client-server models Automation of verification processes for complex systems Performance verification including latency properties Reliable cryptographic code implementation Analysis of his publications reveals strong emphasis on: developing automated verification tools (Armada, Vale, IronFleet), creating novel replication protocols (Aegean), verifying performance characteristics (Performal), and improving specification reliability (IronSpec). His work consistently bridges theoretical formal methods with practical systems implementation. Awards and honors include: Jay Lepreau Best Paper Award at OSDI 2025 Jon R. and Beverly S. Holt Award for Excellence in Teaching (2022) NSF CAREER Award (2021) Distinguished Paper Award at PLDI 2020 Google Faculty Award (2017) Distinguished Paper Award at USENIX Security 2017 Grant support includes NSF FMitF grants (2020, 2023), NSF Large grant (2021), DARPA grant (2020), and Google Faculty Award (2017). He advises PhD students through the GLaDOS group, focusing on distributed systems verification. He directs the GLaDOS lab at University of Michigan, developing verification frameworks and reliable distributed systems. Current projects include automated proof generation (Basilisk) and efficient communication protocols (Scrooge).
Pavel Panchekha is an Assistant Professor in the School of Computing at the University of Utah, where he holds the Warnock Chair for Junior Faculty. His research spans programming languages, web browsers, and numerical analysis, with a focus on developing programming language techniques to address challenges across computer science. Dr. Panchekha received his educational training at prestigious institutions: PhD in Computer Science from the Paul G. Allen School for Computer Science and Engineering at the University of Washington, advised by Michael D. Ernst and Zachary Tatlock BS in Mathematics from MIT Panchekha's research program has two major thrusts. First, he works on web browser internals , with projects including fuzzing layout invalidation, multi-tenant garbage collection, and optimizing 2D graphics. He is also authoring a textbook on web browsers that informs much of this research. Second, he focuses on automatic numerical analysis , with projects such as automatic accuracy improvement, synthesis via term rewriting, scalable static accuracy analysis, and math library implementation. He leads the FPBench and Herbie projects, which are major deployments of his research. His scholarly output demonstrates consistent contributions across programming languages, verification, and numerical methods. Recent work shows a growing emphasis on bidirectional typing systems, layout invalidation in browsers, and robust floating-point error analysis. His publications reveal a trajectory from foundational work on floating-point accuracy (notably the Herbie tool that won a Distinguished Paper Award at PLDI 2015) toward more comprehensive systems for program synthesis, verification, and browser optimization. Panchekha has received significant recognition for his research contributions: NSF Fellowship ARCS Foundation Fellowship Adobe Research Fellowship Wissner-Slivka Foundation Fellowship 2015 PLDI Distinguished Paper Award for work on the Herbie numerical analysis and repair tool As an advisor, Panchekha mentors a substantial group of students across multiple levels. He currently advises six students: Marisa Kirisame (PhD), Bhargav Kulkarni (PhD), Yumeng He (PhD), Artem Yadrov (MS), Jesus Ponce (BS), and Jonas Regehr (BS). Previously, he has advised over twenty students including PhD candidates like Ian Briggs and numerous MS and BS students. His advising spans theoretical topics in programming languages and practical applications in web browsers and numerical computing. Panchekha leads research groups focused on programming languages applications to web browsers and numerical analysis. His work on the Herbie tool for floating-point accuracy improvement has become influential in the programming languages community, and his more recent work on browser internals is shaping how researchers understand and optimize modern web rendering engines. He is currently developing a textbook on web browsers that aims to synthesize knowledge about browser architecture and implementation.
Riyadh Baghdadi is an Assistant Professor of Computer Science at New York University Abu Dhabi and a Global Network Assistant Professor at the Tandon School of Engineering, NYU. He is also a Research Affiliate at MIT, where he previously completed a postdoctoral fellowship. His academic journey includes a PhD and Master’s from Sorbonne University (INRIA/UPMC) and an engineering degree from Ecole Supérieure d’Informatique in Algiers. Assistant Professor, NYU Abu Dhabi Global Network Assistant Professor, Tandon School of Engineering, NYU Research Affiliate, MIT His research lies at the intersection of compilers, programming languages, and applied machine learning, with a focus on developing advanced compiler techniques for deep learning, high-performance computing, and data-parallel algorithms. He is the lead developer of the Tiramisu compiler , a polyhedral compiler designed to optimize dense and sparse deep learning workloads across diverse architectures including CPUs, GPUs, and FPGAs. Riyadh’s recent publications demonstrate a strong trend toward integrating machine learning into compiler optimization—particularly in cost modeling, loop scheduling, and automatic code generation. His work addresses critical challenges in optimizing sparse neural networks and enabling efficient execution on resource-constrained platforms like smartphones and autonomous vehicles. Outstanding Paper Award, MLSys 2021 He has mentored 18 students and taught core courses such as Computer Systems Organization and Machine Learning at NYUAD. His service to the academic community includes program committee roles at MLSys, IPDPS, ECOOP, and PACT, as well as organizing workshops on polyhedral compilation and machine learning for hardware-software co-design. Riyadh actively contributes to open-source projects and collaborates with industry leaders including Google, Facebook, NVIDIA, and Intel. He leads the development of Tiramisu and collaborates on DSLs like GraphIt and Halide, focusing on performance portability and automation in compiler design.
Matthieu Sozeau is a prominent researcher at Inria in the Gallinette team in Nantes, France, and a key contributor and coordinator of the Coq/Rocq proof assistant project. His work bridges theoretical computer science and practical software development, focusing on creating reliable formal verification tools. His research interests span Type Theory, Proof Assistants, Functional Programming, and Unification. He has made significant contributions to the development of Coq (recently renamed to Rocq Prover), particularly through the MetaCoq project which aims to verify Coq's kernel within Coq itself, the Equations plugin for dependent pattern matching, and CertiCoq, a verified compiler from Coq to assembly. His work enables stronger guarantees about formalized mathematics and verified software. Sozeau's publications reveal a consistent focus on foundational aspects of proof assistants. His recent work includes verified type checking ('Coq Coq Correct!'), verified extraction from Coq to OCaml, and sort polymorphism for proof assistants. These contributions advance both theoretical understanding and practical implementation of dependently-typed programming languages. Distinguished paper award for Verified Compilation from Coq to OCaml at PLDI'24 As an academic mentor, Sozeau has supervised PhD students including Théo Winterhalter and Antoine Allioux. He regularly teaches courses on proof assistants, notably at MPRI (Master Parisien de Recherche en Informatique), and actively participates in the academic community through program committees, invited talks, and workshops. His work has significantly influenced both the theoretical foundations and practical applications of interactive theorem proving.
Andreas Lööw is a Lecturer at Royal Holloway, University of London , focusing on hardware and software verification. Previously, he was a postdoctoral researcher at Imperial College London under Philippa Gardner , contributing to the Gillian Platform . He completed his PhD at Chalmers University of Technology under Magnus Myreen , specializing in interactive theorem proving and hardware verification. His research explores symbolic execution, separation logic, and formal verification of hardware/software systems. Key projects include Betterlog (Verilog semantics reformulation) and foundational work on the Gillian Platform . 2025 : Compositional Symbolic Execution for Memory Models 2025 : Simulation Semantics of Synthesisable Verilog 2024 : Compositional Symbolic Execution for Correctness/Incorrectness 2023 : Exact Separation Logic (Distinguished Paper at ECOOP'24) 2023 : Hardware Verification of Pipelined Processors 2022 : Verilog Concurrency Analysis 2021 : Verified Verilog Compiler (Lutsig) Scientific Awards : Distinguished Paper at ECOOP 2024 He maintains the vv Verilog visualization tool and collaborates on the Gillian Platform . Contact: andreas.loow@rhul.ac.uk
