Todd Millstein is a Professor in the Computer Science Department at the University of California, Los Angeles (UCLA), and served as Department Chair from 2022–2025. He is also an Amazon Scholar and a co-founder and former Chief Scientist of Intentionet (now at AWS). His research focuses on making software systems more reliable, particularly through network verification and programming language techniques. He pioneered the Batfish network configuration analyzer, which is used by AWS, Oracle Cloud, and dozens of companies, and received the ACM SIGCOMM Networking Systems Award (2025) for this work. His recent publications span probabilistic programming, network reliability, and interactive program verification, including papers at PLDI 2024 (on bit blasting probabilistic programs), NSDI 2024 (on behavioral testing of BGP), and HotNets 2024 (on network layering). Todd has received prestigious awards such as an NSF CAREER Award , a Microsoft Research Outstanding Collaborator Award , and multiple best paper awards at PLDI, OOPSLA, and SIGCOMM. He has advised Ph.D. students like Ana Brendel and Poorva Garg , and teaches courses such as CS30 (Principles of Computing), CS231 (Types and Programming Languages), and CS239 (Current Topics in PL and Systems). His professional roles include Program Chair for OOPSLA 2014 and ECOOP 2018, and committee member for numerous conferences including PLDI , SPLASH , and LAFI .
Conrad Watt is an Assistant Professor at Nanyang Technological University (NTU), Singapore , specializing in WebAssembly, formal verification, and concurrency. He previously served as a Research Fellow at Peterhouse, University of Cambridge, and earned his PhD under Peter Sewell. Co-chair of the W3C WebAssembly Community Group Active in WebAssembly standards development, including concurrency specifications Developed mechanizations in theorem provers like Isabelle/HOL Collaborator with industry (wasmtime engine) and academic teams on verification tools Research Focus: Formal verification of low-level languages, concurrency models, and security mechanisms for WebAssembly. His work bridges theoretical rigor with practical applications, including WasmRef-Isabelle and threads projects. Recent Trends: 2025 publications explore separation logic automation and concurrency experiments, while 2024-2023 work emphasizes specification toolchains (SpecTec), verified interpreters, and memory-safe execution techniques. Scientific Awards ACM Doctoral Dissertation Award Honorable Mention EAPLS Best Dissertation Award Advising: Supervises PhD students Qiyuan Xu and Antanas Kalkauskas. Collaborates with researchers like Philippa Gardner and Jean Pichon-Pharabod.
Alastair F. Donaldson is a Professor and Director of Research in the Department of Computing at Imperial College London, where he leads the FastPL research group. His work bridges formal methods, software testing, and programming languages, with a focus on enhancing the reliability of high-performance and parallel software systems. He has held key roles including Director of Research (since 2023) and previously served as Lecturer (2011–2014), Senior Lecturer (2014–2017), and Reader (2017–2020) before being promoted to Professor in 2020. His research interests include formal verification, compiler testing, GPU programming, concurrency, and fuzzing. He has made significant contributions to the verification of GPU kernels, metamorphic testing of graphics drivers, and the development of tools like GPUVerify and GraphicsFuzz. His work combines theoretical rigor with practical impact, demonstrated by the acquisition of his startup GraphicsFuzz by Google in 2018 and his subsequent roles as Senior Software Engineer and Visiting Researcher at Google. His recent publications reflect a sustained focus on compiler and system reliability, with trends in fuzzing, formal specification, and automated testing of complex systems such as WebGPU, CXL cache coherence, and large language models for code generation. His work increasingly integrates empirical validation with formal techniques to uncover subtle bugs in real-world systems. Scientific awards and recognitions include: 2017 BCS Roger Needham Award EPSRC Early Career Fellowship Fellow of the British Computer Society Best Paper awards at EuroSys 2024, MET 2021, IISWC 2019, IWOCL 2019, and ICST 2016 Best Industry Paper at ICST 2024 ACM SIGSOFT Distinguished Paper at ISSTA 2023 ACM SIGPLAN Most Influential OOPSLA Paper Award (2012 paper), awarded in 2022 Best Student Paper at PPoPP 2014 He has advised numerous PhD students and leads a vibrant research group. He has secured significant research funding and collaborates extensively with industry and academia. His service includes leadership roles such as General Chair of PLDI 2020, PC Chair of ECOOP 2019, and Steering Committee Chair of PLDI (2022–2025). He also serves on the advisory board of PACM-PL and on program committees for top venues including POPL, OOPSLA, PLDI, ICSE, and ISSTA. He leads the FastPL research group, which focuses on the design and implementation of programming tools and techniques for reliable software. The group conducts cutting-edge research in compiler testing, formal methods, and high-performance systems, fostering collaboration across academia and industry.
Danfeng Zhang is a faculty member at Duke University whose research sits at the intersection of programming languages and security. Active across the premier PL conferences since 2015, Zhang has served on more than two-dozen program committees and currently co-chairs the POPL Student Research Competition. Education & Affiliation: Home page: users.cs.duke.edu/~dz132 Affiliation: Duke University, United States Research Interests: Zhang’s work spans programming-language design, static and dynamic analysis, formal verification, and security. A recurring theme is developing language-based techniques that guarantee strong security and privacy properties—ranging from side-channel resistance and constant-time execution to differential-privacy proofs—while preserving performance and usability. His recent projects combine type systems, program logics, and automated reasoning to build practical verification tools for concurrent, speculative, and approximate software. Publication Trends: Across nine representative papers (2015-2024) Zhang has advanced static detection of cache side channels, automated proofs of differential privacy, and relaxed concurrency models. The trajectory shows deepening integration of security concerns into language infrastructure, with tool-building (CtChecker, SpecSafe, LightDP) that bridge formal guarantees and real-world systems. Service & Leadership: 2024 POPL Student Research Competition Co-Chair 2025 POPL Program Committee member Repeated reviewer/PC member: PLDI, SPLASH/OOPSLA, ISSTA, ECOOP, APLAS, PriSC, PASS Zhang regularly mentors student researchers through SRC sessions and workshop panels, fostering diversity and early-career participation in the programming-languages community.
Talia Ringer is an Assistant Professor in the Department of Computer Science at the University of Illinois, where she is a member of the PL/FM/SE (Programming Languages/Formal Methods/Software Engineering) research group. She leads the Illinois Theorem Provers (ITP) lab, which focuses on advancing proof engineering technologies to make formal verification accessible to programmers of all skill levels across all domains. Research Interests Dr. Ringer's research spans multiple aspects of proof engineering with a strong focus on integrating techniques from dependent type theory, program transformations, and neural proof synthesis to solve real-world verification challenges. Her work addresses how to build systems that allow programmers to prove the absence of costly or dangerous bugs in software. She is particularly interested in proof repair, machine learning for proofs, and developing new methodologies that can drive the creation of large, secure, and robust verified software and hardware systems. Research Trends Dr. Ringer's recent publications demonstrate a strong shift toward integrating machine learning with formal verification, particularly in proof repair and synthesis. Her work explores how large language models can assist with theorem proving, how reinforcement learning can automate verification processes, and how to make proof engineering more practical for real humans. Many publications involve collaborations with students and researchers from multiple institutions, reflecting her commitment to interdisciplinary research. Awards and Recognition Distinguished Paper Award at ESEC/FSE 2023 for "Baldur: Whole-Proof Generation and Repair with Large Language Models" ACM SIGPLAN Distinguished Service Award in 2023 Mentoring and Service Dr. Ringer is a dedicated mentor who has advised numerous undergraduate and graduate students. She is the founder and president of the Computing Connections Fellowship, which provides transitional funding for computer science PhD students needing to escape unhealthy environments. She is also the founder and previous chair of the SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), which connects more than 200 mentors and 300 mentees across more than 44 countries. Her service work was formally recognized with the 2023 ACM SIGPLAN Distinguished Service Award. Laboratory and Collaborations Dr. Ringer leads the Illinois Theorem Provers (ITP) lab with current members including postdocs, PhD students, masters students, and undergraduates. She collaborates extensively with researchers at the University of Washington, UMass Amherst, Google Research, Galois, and other institutions on various proof engineering projects.
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
Loris D'Antoni is an Associate Professor in the Department of Computer Science and Engineering at the University of California at San Diego (UCSD) . He is also a Visiting Academic at Amazon Web Services (AWS) . His research focuses on helping people write trustworthy software through techniques in program synthesis, formal verification, and machine learning robustness. Bachelor and Master in Computer Science from University of Torino (2008, 2010) PhD in Computer Science from University of Pennsylvania (2015) His research integrates programming languages , automata theory , and formal methods to ensure software reliability. Recent work explores semantics-guided synthesis and specification-aligned LLMs , with applications in network security, machine learning fairness, and automated code repair. Key trends in his publications include program synthesis , formal verification , and trustworthy AI systems . He has contributed to tools like AutomataTutor and SemGuS , a framework for customizable synthesis problems using constrained Horn clauses. Phillip R. Certain-Gary D. Sandefur Distinguished Faculty Award NSF CAREER Award Microsoft Research Faculty Fellowship Google and Facebook Faculty Awards Best Paper Award at ICDCN 2023 Distinguished Paper Award at SBES 2021 D'Antoni actively contributes to academic community service as a committee member in PLDI , OOPSLA , POPL , and CAV . He leads the Programming Systems Group at UCSD and collaborates with SemGuS research team on synthesis frameworks.
John Wawrzynek is a Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He is affiliated with the Department of Electrical Engineering and Computer Sciences in the College of Engineering and serves as Co-Director of the Berkeley Wireless Research Center and Co-PI of the CONIX Research Center, one of the six centers in the Joint University Microelectronics Program sponsored by DARPA. Dr. Wawrzynek received his B.S. in Electrical Engineering from SUNY, Buffalo (1977), M.S. in EE from the University of Illinois, Urbana/Champaign (1979), and Ph.D. in Computer Science from Caltech (1987). Before joining the Berkeley faculty in 1988, he worked as a consultant at Schlumberger Palo Alto Research. His research focuses on Computer Architecture, Reconfigurable Computing, Wireless Systems, and Integrated Circuit and System Design . His work spans both theoretical foundations and practical implementations, with particular emphasis on FPGA-based computing systems, reconfigurable architectures, and wireless communication systems. His research group has made significant contributions to the field of reconfigurable computing, including the development of the Garp architecture and various tools for reconfigurable computing systems. Analysis of his recent publications (2022-2025) reveals continued focus on reconfigurable computing, FPGA design, wireless networking, and formal methods for hardware verification. His work shows an evolution from traditional computer architecture towards specialized hardware acceleration, machine learning for EDA, and wireless systems research, with particular emphasis on SAT sampling, differentiable computing, and efficient FPGA implementation of neural networks. DAC's Most Influential Paper Award (2025) NSF Presidential Young Investigator (PYI) (1989) Charles Lee Powell Fellowship (1985) NASA Certificate of Recognition (1983) Rensselaer Engineering and Science Medal (1975) Professor Wawrzynek has advised numerous graduate students throughout his career, many of whom have gone on to prominent positions in both industry and academia including Google, Xilinx, and MIT Lincoln Laboratory. His research has been supported by various grants from NSF, DARPA, and industry partners. He leads the Berkeley Wireless Research Center, which focuses on next-generation wireless communication systems and technologies, and is actively involved in the CONIX Research Center which explores connected intelligence at the network's edge.
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.
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.
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.
Rodrigo Otoni is an Assistant Professor at the University of Groningen's Faculty of Science and Engineering, affiliated with the Bernoulli Institute for Mathematics, Computer Science, and Artificial Intelligence. His research focuses on automated reasoning for verification, synthesis, and certification in computer science. He leads initiatives in formal methods for distributed systems and maintains active profiles on GitHub and LinkedIn. Research Interests: Specializes in theoretical computer science foundations with applied work in model checking and formal verification. Key areas include: Automated theorem proving for system certification Formal specification of distributed protocols Rigorous verification methodologies for concurrent systems
Sean Welleck is an Assistant Professor at Carnegie Mellon University's School of Computer Science, specifically within the Language Technologies Institute (LTI). He leads the L3 Lab and serves as an advisor for the AI for Math Fund. His academic journey includes a PhD from New York University under Kyunghyun Cho and postdoctoral positions at the Allen Institute for Artificial Intelligence and the University of Washington with Yejin Choi. Dr. Welleck's educational background shows a strong foundation in computer science. He earned his PhD in Computer Science from New York University, where he worked under the mentorship of Kyunghyun Cho and Zheng Zhang. Prior to this, he completed his MSE and BSE in Computer Science from the University of Pennsylvania, demonstrating a long-standing commitment to the field. Dr. Welleck's research focuses on bridging informal and formal reasoning with AI, with particular emphasis on developing learning, inference, and evaluation algorithms for large language models. His work spans multiple cutting-edge areas including mathematical reasoning , code generation , inference algorithms , and AI reasoning agents . A significant portion of his recent work involves combining AI with formal methods for mathematics, where he has developed frameworks like Llemma (an open-source language model for mathematical reasoning) and meta-generation (for inference-time algorithms). His research is characterized by a strong theoretical foundation coupled with practical applications that push the boundaries of what AI systems can achieve in formal reasoning domains. Analysis of Dr. Welleck's recent publications reveals a clear research trajectory focused on enhancing language models' capabilities in formal reasoning and mathematical problem-solving. His work demonstrates an evolution from foundational research in neural text generation to increasingly sophisticated approaches that integrate formal methods with deep learning. Key trends include the development of inference-time algorithms that improve model performance without additional training, frameworks for mathematical reasoning that connect informal and formal proofs, and novel evaluation methodologies for language models. His publications consistently appear in top-tier conferences including NeurIPS, ICLR, ICML, and ACL, reflecting the high impact of his contributions to the field. Dr. Welleck's scientific achievements have been recognized with several prestigious awards: NAACL 2025 Best Paper Award ICLR 2025 Oral Presentation (Top 2%) ICLR 2025 Spotlight Presentation (Top 5%) NeurIPS 2021 Outstanding Paper Award (Top 0.1%) for MAUVE NVIDIA AI Labs Pioneering Research Award (2017 and 2018) As an educator and mentor, Dr. Welleck actively guides the next generation of AI researchers. He currently advises multiple PhD students including Pranjal Aggarwal, Weihua Du, Andre He, and Seungone Kim (some co-advised with other faculty), along with MS students Riyaz Ahuja, Jiewen Hu, Qinyue Tan, and Thomas Zhu, and undergraduate Tate Rowney. At CMU, he teaches advanced courses such as Neural Code Generation and Advanced NLP, and has previously taught at New York University and the University of Washington. His commitment to education extends to creating resources like the Thesis Review Podcast and developing tutorials on neural theorem proving that have been presented at major conferences. Dr. Welleck leads the L3 Lab at CMU, which focuses on the intersection of language, learning, and logic. The lab brings together students and researchers to tackle challenging problems in AI reasoning, with particular emphasis on mathematical reasoning and code generation. Recent initiatives include the development of Llemma, an open-source language model specialized for mathematical reasoning, and work on inference-time algorithms that enable language models to improve their performance through additional computation during inference rather than through additional training.
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
