Marco Vassena is an Assistant Professor at the Department of Information and Computing Sciences, Utrecht University, within the Faculty of Science. He focuses on developing principled methods for building secure systems, bridging Security and Programming Languages research communities. His work applies type systems, compilers, program analysis, and verification to ensure reliable security guarantees in software systems. PhD in Computer Science from Chalmers University of Technology Visiting Assistant Professor at Stanford Postdoctoral Researcher at CISPA Helmholtz Center for Information Security Member of the CISPA-Stanford Center for Cybersecurity His research spans language-based security (constant-time programming, memory safety, information flow control), software defenses against Spectre and side-channel attacks, and WebAssembly sandboxing. He leads projects like MSWasm and Blade, targeting microarchitectural attack mitigation through formal verification and compiler design. Scientific recognition includes the Veni Grant (2023). Current projects explore speculative execution security, dynamic information flow control, and secure WebAssembly implementations.
Dr. Fabrizio De Santis serves as a Part-Time Lecturer at the Technical University of Munich (TUM) within the Chair of Security in Information Technology, while maintaining his primary professional role at Siemens AG in Munich. He teaches the course Advanced Cryptographic Implementations , bridging industrial expertise with academic instruction. His research focuses on practical cryptographic engineering and hardware security, including: Secure implementation of cryptographic algorithms Mitigation of side-channel vulnerabilities Post-quantum cryptographic systems Hardware-based security solutions for embedded systems No scientific awards or student advising activities are documented in available records. His industry position at Siemens provides real-world context for his academic contributions, though no laboratory affiliations or grant details are specified.
Oleksandr Ivanovych Vorobets serves as an Associate Professor in the Department of Computer Systems and Networks at Chernivtsi National University. He holds the academic degree of Candidate of Physical and Mathematical Sciences, awarded for his 2007 PhD thesis on modifying metal-chalcogenide semiconductor barrier structures using pulsed laser irradiation. His academic foundation was built at Yuriy Fedkovych Chernivtsi State University, where he graduated from the Faculty of Physics, Department of Microelectronics and Semiconductor Devices. Research interests span semiconductor device physics , signal processing , and computer engineering , with a focus on modeling and algorithmizing primary information signal converters based on semiconductor barrier structures. His work integrates laser processing techniques for manipulating structural defects in semiconductors and developing hardware/software systems for instrumentation and control. Analysis of his publication history reveals two distinct phases: early work (2003-2009) concentrated on semiconductor material science and laser defect engineering in cadmium telluride structures, while recent publications (2015-2018) pivot toward cryptographic hardware design for IoT and telemetry applications, featuring reconfigurable coprocessors and stream ciphers. Vorobets instructs core computer engineering courses including Computer Electronics, Computer Circuit Engineering, Computer Architecture, System Programming, Microcontrollers, and Automation of Technological Processes and Measurements. His email contact is o.vorobets@chnu.edu.ua.
Aleksandar Jurišić is a Full Professor at the Faculty of Computer and Information Science, University of Ljubljana, where he serves as Head of the Laboratory for Cryptography and Computer Security. He also maintains an affiliation with the Institute of Mathematics, Physics and Mechanics (IMFM) in Ljubljana and occasionally teaches at the Faculty of Mathematics. His educational background includes: B.A. from University of Ljubljana (1987), working under Joze Vrabec on topology applications in combinatorics M.Sc. (1990) and Ph.D. (1995) from University of Waterloo, working under Chris Godsil in algebraic combinatorics Jurišić's research interests focus on Algebraic Combinatorics, Cryptography, and Algorithmic Number Theory . His work bridges theoretical mathematics with practical security applications, particularly in elliptic curve cryptography and finite field implementations. He has made notable contributions to understanding mathematical phenomena like the Mercedes knot problem, which connects everyday observations with advanced mathematical concepts. His publications demonstrate a consistent focus on cryptographic implementations, particularly for resource-constrained environments like smart cards. His research spans theoretical mathematics (knot theory, combinatorics) to applied cryptography, showing how abstract mathematical concepts can solve practical security problems. Among his scientific recognitions , he received the Hasse Prize for his paper 'The Mercedes knot problem' published in American Mathematical Monthly. In 2005, he co-founded the Slovenian Society of Cryptology, demonstrating leadership in establishing cryptography as a field in Slovenia. As an educator and mentor , Jurišić has supervised over 25 diploma theses, 4 master's theses, and 1 PhD dissertation. His courses include Probability and Statistics, Cryptography and Computer Security, and Introduction to Probability and Statistics. He has led numerous educational projects focused on e-content development for mathematics and cryptography education. He leads the Laboratory for Cryptography and Computer Security , which has been involved in multiple Structural Funds projects including PKP series (e-content in education), NA-MA POTI (mathematical literacy), and ŠIPK 1 (Cryptogram - a portal for cryptography and computer security).
Håvard Raddum serves as Chief Research Scientist in the Department of Cryptography at Simula UiB, a joint research entity of Simula Research Laboratory and the University of Bergen. His primary focus involves advancing cryptographic security through algorithm analysis, Fully Homomorphic Encryption applications, and hardware-level attack mitigation. Raddum's research spans cryptography with specialization in security analysis of cryptographic algorithms, practical deployment of Fully Homomorphic Encryption, and physical attacks on hardware implementations. His work addresses vulnerabilities in symmetric ciphers, multivariate schemes, and lattice-based systems through algebraic cryptanalysis, side-channel techniques, and theoretical security proofs. Analysis of his 2019-2025 publications reveals concentrated expertise in cryptanalysis across diverse primitives. Key trends include algebraic attacks on arithmetization-oriented cryptography, side-channel analysis of lightweight ciphers, error detection in lattice computations, and security evaluations of Fully Homomorphic Encryption. His research consistently bridges theoretical frameworks with practical implementation vulnerabilities.
Prof. Dr. Kerstin Lemke-Rust is a Professor at the Department of Computer Science at Bonn-Rhein-Sieg University of Applied Sciences (H-BRS) and a key member of the Institute for Cyber Security and Privacy (ICSP). Her affiliations include leadership roles in the Gesellschaft für Informatik (GI) and the International Organisation for Cryptologic Research (IACR). Her research spans: Cryptographic algorithm security (side-channel/fault analysis) Blockchain and IoT security Automotive cybersecurity Hardware vulnerability detection She teaches courses in IT Security, Applied Cryptography, and Embedded Systems across bachelor’s and master’s programs. Recent publications (2021-2025) focus on blockchain privacy, side-channel attacks, and hardware security, reflecting her emphasis on real-world cryptographic vulnerabilities. She leads research initiatives at ICSP and collaborates internationally on cybersecurity projects.
Dr. Robert Smyk is an Assistant Professor in the Department of Automation at Gdańsk University of Technology's Faculty of Electrical and Automation Engineering. His office is located on floor 112 of the faculty building, and he can be contacted via email at robert.smyk@pg.edu.pl or by phone at +48 58 347 1332. Dr. Smyk's research spans several interconnected domains: Hardware-focused computing : FPGA implementations, residue arithmetic systems, and high-speed digital converters Algorithm development : Novel approaches to residue number system operations and signal processing optimizations Engineering applications : Computer vision for infrastructure inspection, cryptographic systems, and sensor data processing His publications demonstrate consistent focus on improving computational efficiency through mathematical optimizations and hardware-aware designs. With 67 publications documented in institutional repositories, his recent works explore: algorithmic improvements for residue arithmetic (2023-2025), thresholding/edge detection for industrial vision systems (2018-2022), and hardware architectures for specialized converters. Teaching activities include extensive involvement with 163 documented educational engagements.
Matteo Busi is a researcher at University Ca' Foscari Venice , specializing in software security, language-based security, and secure compilation. His work focuses on formal verification of security properties in cryptographic implementations and protocol verification using symbolic methods. Research interests include: Software Security Language-Based Security Secure Compilation Formal Verification Cryptographic Protocol Analysis Embedded Security Recent publications examine constant-time preservation under obfuscation, remote attestation protocols using pi-calculus, and robust compilation techniques. His contributions span POPL, PriSC, and APLAS conferences from 2019 to 2024.
Qirun Zhang is the Catherine M. and James E. Allchin Early Career Associate Professor in the School of Computer Science at Georgia Institute of Technology. His research focuses on program analysis, compiler optimization, and formal language theory, with numerous publications in top-tier programming language and software engineering conferences including PLDI, POPL, OOPSLA, and FSE. He teaches courses on compilers, program analysis, and software testing. Dr. Zhang's research interests center on improving software reliability and security through advanced program analysis techniques. He approaches problems from perspectives including computational complexity, analytic combinatorics, graph theory, and formal languages. His work often bridges theoretical foundations with practical applications in compiler design and program verification. His recent publications show a strong focus on context-free language reachability, Dyck-language based analyses, and SMT solving techniques. His research demonstrates consistent innovation in making program analysis more precise while maintaining scalability, with applications ranging from debug information validation to software debloating and type inference. PLDI Distinguished Paper Award (2020) SIGSOFT Distinguished Paper Award (2023) OOPSLA Distinguished Artifact Award (2022) Dr. Zhang actively mentors PhD and MS students, with current advisees including Camille Bossut and Benjamin Mikek. His service to the academic community includes Artifact Evaluation Co-Chair roles for PLDI 2025 and 2026, and program committee membership for numerous top conferences including PLDI, POPL, and OOPSLA. He leads research projects including SLOT, Context-Free Language Reachability with Transitive Redundancy Elimination, and Debug Information Validation.
Adam Chlipala is a Professor at the Massachusetts Institute of Technology working at the intersection of programming languages, formal methods, and computer systems. His research focuses on building practical verified systems with end-to-end machine-checked proofs, particularly using the Coq proof assistant. His educational background includes a Computer Science undergraduate degree from Carnegie Mellon University (2003) and a PhD in Computer Science from the University of California, Berkeley (2007). Following a postdoctoral position at Harvard University through 2011, he joined MIT as faculty. Chlipala's research spans multiple domains with strong emphasis on dependent types , verified compilation , and hardware-software co-verification . His work consistently bridges theoretical foundations with practical implementation, as evidenced by his development of the Ur/Web programming language and his focus on creating clean-slate hardware-software stacks with formal guarantees. Key research thrusts include cryptographic constant-time verification, side-channel security, and verified tensor compilation. His recent publications (2020-2025) reveal a clear trajectory toward increasingly complex verified systems, with growing emphasis on hardware-software integration, cryptographic implementations, and performance-critical applications. The work consistently leverages Coq for machine-checked proofs while addressing real-world constraints like timing channels and hardware interfaces. Chlipala is the author of the influential textbook Certified Programming with Dependent Types , which serves as a primary educational resource for Coq at numerous institutions worldwide. His professional activities include significant service to the PL community through program committees for major conferences including PLDI, POPL, ICFP, and CPP. He leads research initiatives connecting hardware and software verification, most notably through the DeepSpec project which aims to build fully verified computing stacks. His current work focuses on practical applications of dependent types for business applications through Ur/Web and verified cryptographic implementations.
Byron Cook is Professor of Computer Science at University College London (UCL) and Director of Automated Reasoning at Amazon Web Services. He leads Amazon's Automated Reasoning Group (ARG) and has driven the broad adoption of formal methods across AWS services. His career spans academia and industry, with significant contributions to program verification and automated reasoning. His research focuses on verification, automated reasoning, program analysis, computer/network security, programming languages, theorem proving, logic, and applications to hardware design, operating systems, and biological systems. Cook's work bridges theoretical foundations with practical applications in cloud security and system reliability, particularly through his leadership in applying formal methods to AWS infrastructure. Cook's recent publications demonstrate a strong focus on applying automated reasoning to cloud security challenges, particularly around access control policies, network reachability, and cryptographic implementations. His work shows a clear trajectory from theoretical program verification toward practical security applications in large-scale cloud environments, with emphasis on making formal methods accessible to developers through "one-click" verification tools. Scientific Awards: FREng (Fellow of the Royal Academy of Engineering) As an academic advisor, Cook has mentored numerous PhD students and interns who have gone on to significant careers in programming languages and verification research. His work at Amazon has secured substantial research funding for developing and deploying automated reasoning tools across AWS services. Cook founded and leads Amazon's Automated Reasoning Group (ARG), which develops tools like IAM Access Analyzer, Tiros, Zelkova, and T2. Previously, he managed the Programming Principles and Tools (PPT) group at Microsoft Research Cambridge, where he co-founded projects including TERMINATOR, SLAyer, and the Bio Model Analyzer (BMA).
Bryan Parno is the Kavčić-Moura Professor of Electrical & Computer Engineering and Computer Science at Carnegie Mellon University, where he leads the Secure Foundations Lab within CyLab, CMU's Security & Privacy Institute. His research combines theory and practice to provide formal, rigorous security guarantees about concrete systems, with emphasis on creating solid foundations for practical solutions. His research spans secure systems , formal software verification , applied cryptography , data privacy , and usable security . Current work focuses on protocols for verifiable computation and zero-knowledge proofs, building practical formally verified secure systems, and developing next-generation application models. His lab maintains a strong commitment to reproducibility, open-sourcing code under permissive licenses, and avoiding patenting results to maximize public benefit. His recent publications demonstrate a clear trend toward practical verification of real-world systems, particularly through the Verus project for verifying Rust code, Everest for building verified HTTPS stacks, and Ironclad for provably secure systems. These works bridge the gap between theoretical security guarantees and practical implementation, with applications ranging from blockchain protocols to verified cryptographic libraries deployed in the Linux kernel. His scientific achievements include multiple Distinguished Paper/Artifact Awards (USENIX Security, SOSP, PLDI), the IEEE Cybersecurity Award for Practice , the Sloan Fellowship , and the ACM Doctoral Dissertation Award . His work on verifiable computation protocols has influenced blockchain systems, while his research on secure code execution environments contributed to Intel's SGX and TDX technologies. As an advisor, Parno has mentored numerous PhD students including Aymeric Fromherz (recipient of the ACM SIGSAC Doctoral Dissertation Award) and Jay Bosamiya. His lab receives funding from diverse sources including NSF, industry partners, and security foundations. Notably, his work has been incorporated into Windows 8+, iOS 13+, and the Linux kernel. He also serves in leadership roles including Chair of IEEE Computer Society's Technical Committee on Security & Privacy. The Secure Foundations Lab maintains strong industry connections, with alumni joining Microsoft Research, Inria, Northeastern University, and other leading institutions. Recent projects like Verus, Everest, and Ironclad represent the lab's commitment to building end-to-end verified systems that provide rigorous security guarantees while maintaining practical performance.
Fernando Magno Quintão Pereira is an Associate Professor at the Federal University of Minas Gerais (UFMG), Brazil, specializing in compiler design and program analysis. His academic journey began with a Ph.D. from UCLA in 2008 under Jens Palsberg's supervision, establishing his foundation in compiler research. His research focuses on compilers , with core expertise in code generation , compiler optimizations , and static program analyses . Recent work explores quantum compilation, binary analysis, and security-aware compilation techniques. His publications reveal consistent contributions to major conferences including PLDI, CGO, and SPLASH, with emphasis on practical optimization frameworks and theoretical compiler advancements. Analysis of his 15 most recent publications (2020-2026) shows dominant themes in binary optimization (e.g., AnghaBench), security-aware compilation (e.g., Memory-Safe Elimination of Side Channels), and emerging architecture support (e.g., Quantum Computing Compilation). His work bridges theoretical compiler principles with real-world systems challenges. He actively contributes to the academic community through: Program committees for PLDI (2020-2025), CGO (2021-2026), and SPLASH conferences Leadership roles including CGO Finance Chair (2026) and PLDI Diversity & Inclusion Co-Chair (2023-2024) Organizing JENSFEST 2024 and serving on multiple conference steering committees Pereira maintains an active research group evidenced by continuous publication output and conference leadership, with his personal website ( homepages.dcc.ufmg.br/~fernando/ ) serving as a hub for his academic activities.
Clément Pit-Claudel is an assistant professor at École Polytechnique Fédérale de Lausanne (EPFL) in the School of Computer and Communication Sciences, Department of Computer Science. He leads the SYSTEMF lab which he founded in January 2023. Prior to joining EPFL, he was a PhD candidate at MIT with Adam Chlipala and subsequently worked as a senior applied scientist at Amazon AWS. His academic journey began at École Polytechnique in France, followed by doctoral studies at MIT. Dr. Pit-Claudel's research focuses on programming languages, compilers, and formal verification, with broader interests spanning systems engineering, hardware design languages, security, performance engineering, databases, and type theory. His work centers around three main axes: extensible compilation (teaching compilers domain-specific optimization tricks), hardware design languages and verification, and tooling for proof assistants. He has developed several influential systems including Elk (a linear-time engine for JavaScript regexes), Warblre (a Coq translation of JS regex specification), Fiat (a library for correct-by-construction refinement), Narcissus (for verified binary encoders/decoders), F2F (a program extraction framework), Rupicola (a compiler-construction toolkit), Kôika (a rule-based hardware design language), Cuttlesim (a fast hardware simulator), and Alectryon (a literate programming system for Coq). His publications span top venues including PLDI, POPL, ICFP, ASPLOS, and SLE, with recent work focusing on verified JavaScript regular expressions, foundational integration verification of cryptographic servers, and relational compilation techniques. His research aims to build small, fast, and completely verified components for critical systems through a combination of machine-checked proofs, hardware-software co-design, low-level compiler engineering, and new tools for interactive theorem proving. His notable awards include the Distinguished Artifact award at SLE 2020 for 'Untangling Mechanized Proofs,' the William A. Martin Memorial Thesis Award from MIT in 2016, and the Frederick C. Hennie III Teaching Award from MIT in 2016. He has served on program committees for numerous conferences including PLDI, POPL, ICFP, and SPLASH, and has organized workshops such as the Coq Workshop and Proof Systems. As an educator, he teaches 'Software Construction' (undergraduate level, ~400 students) and 'Interactive Theorem Proving' (graduate level) at EPFL. His teaching philosophy emphasizes hands-on learning, continuous assessment through oral examinations, and designing assignments that lead students to build concrete artifacts they can be proud of. His approach is informed by hundreds of hours of in-class instruction in Europe and the US, resulting in stellar student reviews and multiple teaching awards.
Tamara Rezk is a researcher at Inria (Institut National de Recherche en Informatique et en Automatique) in France, specializing in computer security, programming languages, and formal verification. She has been an active member of the programming languages research community since at least 2015, with significant contributions to top conferences including PLDI, POPL, and ECOOP. Her research focuses on addressing critical security vulnerabilities in modern computing systems, particularly Spectre-class vulnerabilities. She investigates formal methods for ensuring security properties through programming language techniques, compiler security, and verification methodologies. Her work bridges theoretical foundations with practical security concerns in real-world systems. Dr. Rezk has published influential papers on constant-time programming foundations, secure cryptography implementations in the Spectre era, and type systems for information flow security. Her research demonstrates how programming language theory can provide rigorous solutions to hardware-level security flaws. She serves on program committees for major conferences including PLDI, POPL, and the Principles of Secure Compilation (PriSC) workshop, where she has also been a steering committee member. Her organizational contributions include serving as Local Organizing Chair for PriSC 2018 and Organizing Chair for PLMW@PLDI.
