Riad S. Wahby is an Assistant Professor in the Department of Electrical and Computer Engineering at Carnegie Mellon University's College of Engineering. His work focuses on designing secure hardware and software systems, with recent emphasis on cryptographic proof systems. He actively mentors PhD students and collaborates across disciplines in cybersecurity, blockchain, and formal verification. PhD in Computer Science, Stanford University MEng in Electrical Engineering, Massachusetts Institute of Technology SB in Electrical Engineering, Massachusetts Institute of Technology Wahby's research spans cryptography , blockchain security , zero-knowledge proofs , and secure hardware-software co-design . His work addresses challenges in verifiable computation, privacy-preserving protocols, and hardware subversion resistance. Recent publications reveal trends in zero-knowledge proof systems (SNARKs, MPC), blockchain security (anonymous blocklisting, decentralized auctions), and hardware-crypto integration (weird machines, verifiable ASICs). Technical focus areas include formal verification, side-channel analysis, and cryptographic compilers. Distinguished Student Paper Award, IEEE Symposium on Security and Privacy (Oakland16), 2016 Best Paper Award, USENIX Annual Technical Conference (ATC18), 2018 Wahby collaborates with researchers across institutions and industries, including Dan Boneh at Stanford, Mike Walfish at NYU, and Silicon Labs in industrial roles. His CyLab affiliations connect him to over $400K in seed funding opportunities and blockchain initiatives at CMU.
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.
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).
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
Geoffroy Couteau is a CNRS research scientist at IRIF (Institut de Recherche en Informatique Fondamentale), Université Paris Cité, where he conducts research in theoretical and applied cryptography. He obtained his PhD from École Normale Supérieure de Paris in 2017 under the supervision of David Pointcheval and Hoeteck Wee, followed by a postdoctoral position at Karlsruhe Institute of Technology (KIT) from 2017 to 2019. His primary research interests include secure multiparty computation, zero-knowledge proofs, and the theoretical foundations of cryptography, with a particular emphasis on pseudorandom correlation generators and efficiency improvements in cryptographic protocols. He has made significant contributions to fine-grained cryptography, non-interactive zero-knowledge proofs, and post-quantum secure computation. The recent publications reflect a strong trend toward foundational advances in secure computation, with increasing focus on efficiency, practicality, and connections to complexity theory and learning theory. His work often bridges theoretical hardness assumptions with practical protocol design. ERC Starting Grant (2023) for project OBELiSC (Overcoming Barriers and Efficiency Limitations in Secure Computation) Geoffroy Couteau has advised numerous PhD and master’s students, including Dung Bui, Clément Ducros, Eliana Carozza, and Ulysse Léchine. He has also hosted many visiting students and postdocs, fostering a vibrant research group. He has served on the program committees of major conferences such as EUROCRYPT, CRYPTO, TCC, and PKC. He is currently leading research in cryptography at IRIF and is involved in postdoctoral hiring for projects in advanced cryptographic primitives. He maintains a research blog and resource collection for students, including LaTeX templates, a probability cheat sheet, and curated answers to common cryptography questions.
Chris Peikert is a Professor in the Department of Computer Science and Engineering at the University of Michigan's College of Engineering. He received his Ph.D. from MIT's Computer Science and Artificial Intelligence Laboratory in 2006 under the supervision of Silvio Micali. Peikert is a leading researcher in cryptography, particularly known for his foundational work in lattice-based cryptography. His research interests span cryptography, lattices, coding theory, algorithms, and computational complexity, with a particular focus on cryptographic schemes whose security can be based on the apparent intractability of lattice problems. Peikert has made significant contributions to the development and analysis of lattice-based cryptographic primitives, including ring-LWE, fully homomorphic encryption, and zero-knowledge proofs. Peikert's recent work demonstrates continued leadership in post-quantum cryptography, with publications in top venues like CRYPTO, EUROCRYPT, and STOC. His research spans theoretical foundations of lattice problems to practical implementations of lattice-based cryptographic systems, including hardware acceleration for fully homomorphic encryption. IACR Fellow (2024) Test-of-Time Award from Crypto 2008 (2023) TCC Test-of-Time Award (2017) Patrick C. Fischer Development Professor of Theoretical Computer Science (2017) Best Paper Award at Eurocrypt 2010 Best Paper Award at STOC 2009 Alfred P. Sloan Foundation Fellowship Google Research Award Peikert has been actively involved in the cryptographic research community, serving on program committees for major conferences including CRYPTO, EUROCRYPT, FOCS, and TCC (where he was program co-chair in 2021). He has also developed educational resources, including extensive lecture materials on lattice-based cryptography and teaching courses on cryptography and theoretical computer science at both the undergraduate and graduate levels.
Justin Thaler is an Associate Professor in the Department of Computer Science at Georgetown University, researching algorithms and computational complexity with focus on probabilistic proof systems, verifiable computation, and streaming algorithms. Education: PhD Computer Science, Harvard University BS Computer Science and Mathematics, Yale University Research Interests: Develops protocols for verifying computations (including zero-knowledge proofs), analyzes the power of low-degree polynomials, and designs efficient streaming/sketching algorithms for large datasets. Publications: Research advances theoretical foundations of proof systems, with recent work on SNARKs, lookup arguments, and Fiat-Shamir security. Authored the monograph 'Proofs, Arguments, and Zero-Knowledge'. Advising & Labs: Advises PhD students in theoretical computer science. Contributes to open-source projects including DataSketches library of streaming algorithms. Currently on leave at a16z crypto research.
Shuvendu K. Lahiri is a researcher at Microsoft Research, focusing on formal verification, program synthesis, and software testing. His work bridges artificial intelligence with formal methods, particularly in blockchain security and automated code generation. 2025 : Published LLM-Vectorizer (verified loop vectorizer) and neural synthesis for SMT-assisted proof-oriented programming 2024 : Explored LLM-based test-driven code generation and natural precondition inference 2023 : Developed resource management specifications and contributed to test generation with pre-trained models 2022 : Advanced Solidity type systems and merge conflict resolution using language models His research combines large language models with formal verification tools to improve software correctness. He actively contributes to conferences like ICSE, PLDI, and ISSTA as author and committee member.
Dr. Farzaneh Derakhshan is an Assistant Professor in the Computer Science Department at Illinois Institute of Technology (Illinois Tech), where she explores logical foundations of concurrency and develops formal methods for program verification. She earned her Ph.D. in Pure and Applied Logic from Carnegie Mellon University in 2021 under Frank Pfenning, followed by a postdoctoral fellowship at CMU with Limin Jia and Stephanie Balzer. Current affiliation: Illinois Tech (since ~2021) Previous affiliation: Carnegie Mellon University (Ph.D. and postdoc) Research focus: Type theory, logical verification, and security for concurrent systems Teaching: Courses on programming languages, type systems, and security Her research addresses fundamental challenges in concurrent programming, including: Developing modal logic frameworks for system verification Designing type systems for intermittent computing Creating behavioral type systems for security guarantees Applying relational logic to GPU security and secure compilation Investigating logical foundations of session-typed processes Formal verification of cyclic process networks Current research trends include: Hybrid dynamic verification for parallel systems Logical approaches to side-channel security Formal methods for cyber-physical systems Crash-resilient computing models Security verification in decentralized applications Noninterference proofs in session-typed concurrency Scientific recognition: NSF SaTC CORE Collaborative Award #2350217 Organizing committee member at Dagstuhl Seminar 26071 Professional leadership: Program committee co-chair for PLACES 2025 Committee roles at LICS 2026, ESOP 2026, ICFP 2025, and ECOOP 2025 Regular reviewer for ACM Transactions journals Laboratory involvement: Co-director of behavioral types research at Illinois Tech Collaboration with Carnegie Mellon's formal verification group Key participant in the FACCT workshop
Steve Zdancewic is the Schlein Family President's Distinguished Professor and Associate Chair in the Department of Computer and Information Science at the University of Pennsylvania's School of Engineering and Applied Science. He is a leading researcher in programming languages, formal methods, and computer security with over two decades of impactful contributions to the field. His research interests span programming languages, type theory, logic, computer security, quantum programming, and formal verification. Zdancewic has made significant contributions to information-flow security, memory safety, program synthesis, and the verification of low-level systems. His work often bridges theoretical foundations with practical applications, particularly through the development of verified systems using Coq and other proof assistants. Analysis of his recent publications reveals a strong focus on formal verification techniques, particularly using Interaction Trees and the Coq proof assistant. His research trajectory shows consistent evolution from foundational work on information-flow security toward increasingly sophisticated verification of complex systems including LLVM, quantum computing, and distributed systems. His work demonstrates a commitment to building practically useful verification tools while maintaining rigorous theoretical foundations. Distinguished Paper Award for Semantics for Noninterference with Interaction Trees (ECOOP 2023) Schlein Family President's Distinguished Professor (2021) Distinguished Paper Award for Interaction Trees (POPL 2020) Christian R. and Mary F. Lindback Foundation Award for Distinguished Teaching (2018) IEEE MICRO top picks (2013) Alfred P. Sloan Fellow (2009-2010) NSF CAREER award (2004) Zdancewic has advised numerous PhD students who have gone on to successful careers in academia and industry. His research has been supported by significant grants from NSF, including the NSF Expedition on the Science of Deep Specification. He is actively involved in multiple major research projects including Vellvm (verified LLVM), DeepSpec, and quantum programming verification. Zdancewic also co-organizes Penn's PL Club programming languages research group with Benjamin Pierce and Stephanie Weirich.
Éric Tanter is a Full Professor in the Computer Science Department (DCC) at the University of Chile, where he also leads the PLEIAD Lab. He holds an Inria International Chair (2025–2029) and is an Associate Researcher at the Millenium Institute for Foundational Research on Data (IMFD). His academic leadership includes prior roles as Director and Deputy Director of the DCC, and Coordinator of the PhD Program in Computer Science. His research centers on programming languages and software engineering, with a strong focus on gradual typing, type systems, program verification, and secure programming. He explores both theoretical foundations and empirical practices, aiming to bridge the gap between static and dynamic language paradigms. His recent work emphasizes gradual verification, refinement types, and applications in proof assistants and security. The trends in his recent publications show a deep engagement with foundational aspects of gradual and dependent typing, often aiming to enhance the reliability and security of software systems. These works frequently involve formalization in proof assistants like Coq and explore applications in differential privacy, secure interoperability, and symbolic execution. Inria International Chair (2025–2030) Best Paper Awards at POPL 2019, OOPSLA 2018, ICFP 2018, MSR 2011, AOSD 2010, SBLP 2008, DAIS 2006 Most Influential/Most Notable Paper Awards at DLS, Programming, DLS Facebook Research Testing and Verification Award (2018) Google Faculty Research Awards (2015, 2016) Best Professor Award, University of Chile (2011) Éric Tanter has advised numerous PhD and Master’s students, many of whom have gone on to publish influential work in top venues. He has led multiple research projects funded by FONDECYT, ANID, INRIA, and other national and international agencies. His service includes editorial roles in journals such as the Journal of Functional Programming and Science of Computer Programming, and extensive participation in program committees of major conferences like POPL, ICFP, and OOPSLA. He leads the PLEIAD Lab at the University of Chile, a research group focused on programming languages, software engineering, and formal methods. The lab fosters collaboration with international institutions and emphasizes both theoretical rigor and practical impact.
Srinivas Narayana is an Assistant Professor in the Department of Computer Science at Rutgers University, specializing in programmable networking, formal verification, and systems research. He holds a PhD from Princeton University and a B.Tech from IIT Madras, with postdoctoral work at MIT. His research focuses on building safe, high-performance networks through optimizing compilers, verified programming, and distributed system monitoring. He has received NSF grants, the CGO 2022 Distinguished Paper Award, and the 2017 SIGCOMM Best Paper Award. Education: PhD and MA in Computer Science, Princeton University (2016) B.Tech in Computer Science, IIT Madras (2010) Postdoctoral Research, MIT (2018) Research Interests: His work bridges networking and systems with a focus on compilers, formal methods, and programmable hardware. Notable projects include K2 compiler for eBPF, the eBPF verifier soundness work, and congestion control mechanisms like CCP. He explores parallel packet processing, privacy-preserving analytics, and load balancing strategies. Grants & Awards: NSF Awards #2422076, #1910796, #2019302 eBPF Foundation Grant Facebook Networking Research Award Network Programming Initiative (NPI) Funding Lab & Teams: Leads the NetSys group at Rutgers, collaborating with teams on projects like the eBPF verifier, verified packet processing, and network monitoring tools like Marple. His lab emphasizes open-source contributions and industry collaboration.
Zachary Tatlock is an Associate Professor at the Paul G. Allen School of Computer Science & Engineering at the University of Washington, where he leads the Programming Languages & Software Engineering Group (PLSE) and the SAMPL Group. His research spans programming languages, formal verification, compilers, and computational fabrication. He is also an Amazon Scholar with AWS's Automated Reasoning Group and previously advised OctoML. Tatlock's work bridges theoretical foundations with practical systems, focusing on making it easier to write tricky code while ensuring correctness through rigorous proofs and measurements. PhD in Computer Science & Engineering, University of California, San Diego (2014) Thesis: Reducing the Costs of Proof Assistant Based Formal Verification Advisor: Sorin Lerner BS in Computer Science (Honors) and Mathematics, Purdue University (2007) Professor Tatlock's research focuses on the intersection of programming languages, formal methods, and systems. His work in compilers and formal verification aims to make it easier to write tricky code while ensuring correctness through rigorous proofs. He explores computational fabrication techniques that bridge digital design with physical manufacturing. His recent work on equality saturation (via the egg framework) has transformed program optimization and synthesis. Tatlock also investigates floating-point numerics, distributed systems verification, and hardware/software co-design, always seeking to balance theoretical rigor with practical implementation. Tatlock's recent publications demonstrate a strong focus on equality saturation techniques (egg framework), computational fabrication, and verified systems. His work increasingly integrates machine learning with program analysis and synthesis. There's a clear trajectory toward more practical applications of formal methods in real-world systems, particularly in numerical computing and fabrication. His research group has made significant contributions to e-graph technology, floating-point accuracy, and the verification of distributed systems. Distinguished Paper Award for Rewrite Rule Inference Using Equality Saturation (OOPSLA 2021) Spotlight Paper Award for Dynamic Tensor Rematerialization (ICLR 2021) Distinguished Paper Award for egg: Fast and Extensible Equality Saturation (POPL 2021) Faculty Appreciation for Career Education & Training (FACET) Award (2020) NSF CAREER Award: Verifying Distributed System Implementations (2017) Distinguished Paper Award for Automatically Improving Accuracy for Floating Point Expressions (PLDI 2015) Distinguished Teaching Award Nomination (2015) Professor Tatlock has advised numerous doctoral, master's, and undergraduate students who have gone on to prominent positions in academia and industry, including faculty positions at the University of Utah and Brown University, and leadership roles at companies like OctoML and Certora. His research is supported by significant funding from NSF, DARPA, DOE, and industry partners, totaling millions of dollars. Current grants include projects on computer-aided reasoning, formal verification, computational fabrication, and machine learning systems. He has served on numerous program committees and organized workshops including FPTalks, EGRAPHS, and PNW PLSE. As co-leader of the Programming Languages & Software Engineering (PLSE) research group and affiliate of the SAMPL Group at the University of Washington, Tatlock has developed influential tools including egg (an equality saturation toolkit), Carpentry Compiler, and Odyssey. His group actively collaborates with industry partners including Amazon Web Services, where he serves as an Amazon Scholar. The group has made significant contributions to equality saturation, floating-point accuracy, program synthesis, and computational fabrication, with applications ranging from compiler optimization to 3D printing.
Professor Tobias Nipkow is a leading researcher in formal methods and interactive theorem proving at the Technical University of Munich (TUM), affiliated with the School of Computation, Information and Technology and the Department of Computer Science. He is a core developer of the Isabelle proof assistant and leads the Theorem Proving Group. His work has profoundly influenced program verification, semantics, and formalized mathematics. University: Technical University of Munich School: School of Computation, Information and Technology Department: Department of Computer Science Research Group: Theorem Proving Group Key Projects: Isabelle, Archive of Formal Proofs, Concrete Semantics His research focuses on formal verification, higher-order logic, semantics of programming languages, and verified algorithms. He has pioneered the formalization of textbook algorithms, data structures like B+-trees and quadtrees, and logical systems. His work bridges theoretical foundations with practical tools for software correctness. The most recent publications show a strong trend in verifying classical algorithms (e.g., Gale-Shapley, Earley parser), data structures (B+-trees, deques), and decision procedures, primarily using Isabelle/HOL. His contributions span foundational logic, program analysis, and educational approaches to formal methods. Best Paper Award at CADE 28 (2021) Tobias Nipkow has made extensive contributions to advising and collaborative research, co-authoring with numerous researchers and students. He has secured support for large-scale formalization efforts and contributed to major projects like the Flyspeck proof of the Kepler conjecture. His work is supported by ongoing development of the Isabelle framework and the Archive of Formal Proofs. He leads the Theorem Proving Group at TUM, which is central to the development and application of Isabelle. The group fosters international collaboration, contributes to the Archive of Formal Proofs, and advances research in automated reasoning, semantics, and verified systems.
Théo Winterhalter is a researcher at INRIA Saclay and a member of the Laboratory of Mathematics and Computer Science (LMF) at ENS Paris-Saclay . He previously held a postdoctoral position at the Max Planck Institute for Security and Privacy (MPI-SP) and completed his PhD at the Gallinette research team in Nantes, supervised by Nicolas Tabareau and Matthieu Sozeau. Education PhD in Computer Science, 2017–2020, University of Nantes (Gallinette/Inria) MSc in Computer Science, École Normale Supérieure de Rennes Research interests include type theory , proof assistants , formal verification , and dependent types . He actively works on improving the safety and usability of proof assistants like Rocq (formerly Coq), focusing on rewrite rules, erasure, and cryptographic verification. His work often involves formalizing results within proof assistants and developing tools for verified programming. Contributions span conferences like POPL, ICFP, CPP, and TYPES. Recent projects include foundational verification of high-speed cryptography ( The Last Yard ), type-preserving rewrite rules ( The Rewster ), and modular cryptographic proofs ( SSProve ). His publications emphasize formal methods and computational assumptions in type theory. Teaching includes the Proof Assistants course at MPRI , a joint master’s program. He co-supervises PhD students like Yann Leray and has mentored interns on topics such as erased data implementation and Autosubst tooling. Labs and Teams : Deducteam (INRIA Saclay) – Developing deduction tools and formal verification LMF (ENS Paris-Saclay) – Laboratory for Mathematics and Computer Science Gallinette (former) – Team at INRIA Nantes MetaCoq Project – Collaborative effort on Coq verification
