Francesco Leofante is a Research Fellow at Imperial College London , affiliated with the Centre for Explainable AI . His work focuses on Explainable AI (XAI) , particularly counterfactual explanations with formal robustness guarantees against perturbations. Imperial College Research Fellowship DAAD AINet Fellowship (Safety and Security in AI) Imperial PFDC Supporting Research Staff and Students Award 2023 Research Interests center on Explainable AI , emphasizing counterfactual explanations , robustness , model multiplicity , and formal verification in critical systems like energy and aviation. His work bridges AI , formal methods , and human-AI collaboration . Publications include studies on robust counterfactual explanations , parametric ReLUs for verification, and multi-agent systems with formal guarantees. These appear in top venues like AAAI , KR , IJCAI , and AAMAS , often addressing AI safety and trustworthy systems . Scientific Awards include the Imperial PFDC Supporting Research Staff and Students Award 2023 , DAAD AINet Fellowship , and Imperial College Research Fellowship . He also contributes to workshops and program committees at conferences like AAAI, KR, and IJCAI. Future Work includes expanding robust XAI into critical infrastructure systems (energy, aviation) and developing tools like OMTPlan for AI planning and verification .
Cynthia Kop is an Associate Professor in the Software Science group at Radboud University Nijmegen's Institute for Computing and Information Sciences. She holds a prominent position in the academic community with significant contributions to term rewriting systems and their applications in computer science. Her research interests span several interconnected areas of theoretical computer science: Term rewriting systems (both first and higher-order) Implicit computational complexity Program verification and equivalence Constrained rewriting systems Automated reasoning techniques Her recent work demonstrates a clear trajectory toward applying term rewriting techniques to solve practical problems in program verification and complexity analysis. The three most recent publications from 2019 show her focus on constrained rewriting for program equivalence, higher-order dependency frameworks, and cons-free rewriting for implicit complexity characterization. These works represent the intersection of theoretical foundations with practical applications in software verification. Dr. Kop has secured significant research funding through competitive grants including: NWO VIDI project CHORPE (2021-2026): Constrained Higher-Order Rewriting and Program Equivalence NWO TOP project ICHOR (2019-2023): Implicit Complexity through Higher Order Rewriting Marie Curie project HORIP (2015-2017): Higher Order term Rewriting for Intensional Properties She actively supervises PhD students including Liye Guo, Kasper Hagens, and Deivid do Vale, and has developed several influential tools for the rewriting community: WANDA (termination analysis), CTRL (constrained rewriting), and Cora (comprehensive rewriting analysis framework). Her professional service includes chairing the IFIP working group 1.6 on rewriting and serving on numerous program committees for major conferences in her field.
Thomas P. Jensen is a Directeur de recherche (Research Director) at INRIA, the French National Institute for Computer Science and Applied Mathematics. He has been affiliated with INRIA since 2010, previously serving as a researcher at CNRS (French National Center for Scientific Research) from 1993 to 2010. Currently, he leads the Epicure project-team on semantic analysis and compilation for secure execution platforms, and since 2022, he serves as director of the Laboratoire d'Excellence CominLabs. His educational background includes a Cand. scient. in Computing and Mathematics from the University of Copenhagen (1990), a PhD from Imperial College, University of London (1992), and a Habilitation à diriger des recherches from Université Rennes 1 (1999). Dr. Jensen's research focuses on program analysis and software security , with particular expertise in static program analysis based on abstract interpretation theory, language-based security, information flow control, and Software Fault Isolation. His work bridges theoretical foundations with practical applications in secure compilation and program verification. His recent publications reveal a strong trend toward formally verified security mechanisms, particularly in the integration of Software Fault Isolation with verified compilers like CompCert. His research spans both theoretical aspects of program semantics and practical security applications, with increasing emphasis on algebraic data types, relational analysis, and formal verification of program transformations. Best paper award at GPCE 2018 for Verification of High-Level Transformations with Inductive Refinement Types Editor of Strategic research and innovation roadmap for the SPARTA cybersecurity competence network (2022) Dr. Jensen has been actively involved in numerous research projects including JavaSec, Decert, Seccloud, AJACS, Anastasec, SPARTA, and SecurEval. His leadership roles in research teams and projects demonstrate his significant contributions to both academic research and practical cybersecurity applications. His work often involves collaboration with researchers across Europe on large-scale cybersecurity initiatives. He maintains strong connections with the international programming languages and security research communities, regularly publishing in top venues including PLDI, POPL, ICFP, SAS, ESOP, and CSF, and participating in program committees for major conferences in these fields.
Dr. Stephanie Balzer is an Assistant Professor in the Principles of Programming Group at Carnegie Mellon University's School of Computer Science. Her research focuses on enabling failure-free software through formal methods like type systems and verification logics. She emphasizes compositional proofs for scalability and practical validation via software artifacts. Programming Languages Type Theory Program Verification Concurrency & Security Her recent work explores timed protocols, disentanglement logic, and multiparty session types. Articles demonstrate semantic logical relations for termination (2025), deadlock freedom in Rust embeddings (2022), and information flow control (2024). Key collaborative papers address cyclic process networks and separation logic frameworks. Scientific recognition includes: NSF CAREER Award (2025) ACM SIGPLAN Distinguished Paper (2022) ECOOP Distinguished Paper (2022) She supervises PhD candidates Yue Yao, Yinsen Zhang, and Zak Kent (with Guy Blelloch), plus Master's student Sonya Simkin. Former advisee Jules Jacobs received Cum Laude distinction at Radboud University. Active in academic service, Balzer chairs PLMW@POPL workshops and co-organizes Oregon Programming Language Summer School. She serves on program committees for LICS, POPL, and ICFP.
Mohammad Abdollahi Azgomi is a Professor of Computer Engineering at the School of Computer Engineering, Iran University of Science and Technology (IUST), where he has been serving since 2005, progressing from Assistant Professor to Associate Professor and finally to Professor in 2022. He holds multiple significant roles including Director of the Trustworthy Computing Laboratory (TwCL) since 2006, and previously served as Research Deputy of the School of Computer Engineering from 2020-2023. His academic career is complemented by extensive service on editorial boards, scientific committees, and as a PC member for numerous international conferences in security, cryptography, and computer science. Dr. Azgomi earned his Ph.D. in Computer Engineering (Software) from Sharif University of Technology in 2005 with a dissertation on 'High-Level Extensions for Stochastic Activity Networks: Theories, Tools and Applications,' supervised by Prof. Ali Movaghar. He also completed his M.S. (1996, with honors) and B.S. (1991) in Computer Engineering (Software) from the same institution, with his master's thesis focusing on 'Design and Implementation of Security Services for Computer Networks.' His research spans several interconnected domains centered around dependable and secure computing systems. Dr. Azgomi specializes in modeling and simulation techniques, particularly Petri Nets and Stochastic Activity Networks, for quantitative evaluation of system properties. His work significantly contributes to security and privacy frameworks, trust models, and dependable software design. He has pioneered approaches for evaluating cyber-physical systems security through game-theoretic models and developed frameworks for assessing software architecture quality attributes under uncertainty. Analysis of his recent publications reveals a strong research trajectory focusing on computational trust models, malware propagation dynamics in heterogeneous networks, and security evaluation of cyber-physical systems. His work demonstrates consistent application of formal methods like stochastic activity networks and Petri nets to solve complex security and dependability problems. There's a clear progression from foundational modeling techniques to sophisticated applications in cloud computing, web services security, and intrusion-tolerant systems. Best Researcher of the Year, School of Computer Engineering, IUST (2013, 2014, 2016, 2017) Best Paper Award at CSICC'12 for work on symbolic state space generation Best Paper Award at Innovations'09 for security protocol modeling Best Bachelor Thesis Supervisor (2009) Best Lecturer, IT Group, E-Learning Center (2008) Distinguished M.S. Graduate, Sharif University (1996) Dr. Azgomi has supervised an impressive number of doctoral students, with 14 Ph.D. graduates from IUST and 6 from other universities. His current teaching includes graduate courses on Dependable Software Systems and undergraduate Research Methods and Presentation. He serves on the editorial board of the CSI Journal on Computing Science and Information Technology and has been actively involved in numerous international conferences as program committee member and chair. The Trustworthy Computing Laboratory (TwCL), which Dr. Azgomi directs, focuses on rigorous engineering methodologies for evaluating dependability and security in information and communication technologies. The lab conducts research in formal methods, security modeling, dependable systems, and network security, with particular emphasis on Petri nets, stochastic activity networks, and quantitative evaluation techniques for security, privacy, and trust.
Professor Juan P. Garrahan is a distinguished academic in the School of Physics & Astronomy at the University of Nottingham, where he has served as Professor of Physics since 2007. His extensive academic career includes prestigious appointments as a Visiting Fellow at All Souls College, Oxford (2020), Pitzer Visiting Professor at UC Berkeley (2007), and EPSRC Advanced Fellow (2003-2008). He currently holds multiple leadership roles including Postgraduate Admissions Tutor, PGT Senior Tutor, and Director of the Machine Learning in Science (MLiS) MSc program. Garrahan earned his Licenciado in Physics from the University of Buenos Aires in 1992, followed by his PhD from the same institution in 1997. His academic journey continued with postdoctoral work at Oxford (1998-2000), a Glasstone Fellowship (2000-2003), and lecturing positions at Oxford before joining Nottingham. His career progression at Nottingham includes Lecturer (2003-2006), Reader (2006-2007), and Professor (2007-present). Professor Garrahan's research spans the intersection of statistical physics, quantum mechanics, and machine learning. His work focuses on statistical physics of supercooled liquids and glasses , glass transitions and dynamic arrest , quantum non-equilibrium systems , large deviation theory , and statistical mechanics of machine learning . His approach combines theoretical frameworks with practical applications, particularly in understanding complex systems that exhibit glassy behavior. His research has significant implications for materials science, quantum computing, and machine learning algorithms. Analysis of his recent publications reveals a strong trend toward quantum non-equilibrium phenomena, with particular emphasis on connections between glass physics and quantum information. His work increasingly bridges classical statistical mechanics with quantum systems, exploring how concepts like dynamical phase transitions and large deviation theory apply to both domains. The integration of machine learning techniques into traditional physics problems represents another significant trajectory in his recent research. EPSRC Advanced Fellow (2003-2008) Glasstone Fellow (2000-2003) Pitzer Visiting Professor, UC Berkeley (2007) Visiting Fellow, All Souls College, Oxford (2020) Leverhulme Trust Grant recipient (multiple awards) Professor Garrahan has mentored over 15 PhD students to completion, with many now holding faculty positions or prestigious research fellowships. His current research is supported by multiple major grants including EPSRC Grant EP/V031201/1 (2021-2025) and EP/T022140/1 (2021-2024), reflecting the significance and impact of his work. He has successfully secured continuous funding since 2003 through various mechanisms including EPSRC, Leverhulme Trust, and international collaborations. Garrahan leads the Centre for Quantum Non-Equilibrium Systems (CQNE) at Nottingham and has organized numerous high-profile workshops including the 2024 'Machine learning meets many-body physics' conference. His research group includes multiple postdoctoral researchers working on interdisciplinary projects that span statistical physics, quantum information, and machine learning applications. The group maintains strong collaborations with institutions worldwide and regularly hosts visiting scholars through programs like the Leeds-Loughborough-Nottingham Non-Equilibrium Seminars.
Fabrice Boissier is an Associate Professor at EPITA, specializing in digital methods for humanities and social sciences. He earned his PhD and MSc from Université Paris 1 Panthéon-Sorbonne, focusing on knowledge extraction and reuse in knowledge-intensive processes, enterprise modeling for decentralized organizations, and applications of formal concept analysis, natural language processing, and data visualization. Current Research: Formal Concept Analysis, Topic Modeling, Text Processing, Data Visualization, Knowledge Extraction, and Knowledge-Intensive Processes. Collaborations: Working with Nida Meddouri in the Security and Systems team and Marie Puren in the DMHSS (MNSHS) team. Teaching: Courses in algorithmics, computer architecture, programming languages, and operating systems at EPITA's Bachelor CyberSécurité program. Supervision: Mentoring research and industry interns from EPITA, Université de Sousse, and Université Paris 1 Panthéon-Sorbonne.
Benjamin Pierce is the Henry Salvatori Professor in the Department of Computer and Information Science at the University of Pennsylvania. His research spans programming languages, formal verification, and sustainable computing, with a focus on practical applications in software reliability and security. He leads initiatives like Carbon Connect (NSF Expedition in Sustainable Computing) and serves on climate-focused committees such as Penn's Faculty Senate Select Committee on the Climate Emergency. Research Interests Pierce's work integrates theoretical and applied computer science, emphasizing: Programming Languages : Type systems, language-based security, and compiler verification Formal Methods : Computer-assisted verification, proof automation, and property-based testing Sustainability : Reducing computing's environmental impact through algorithmic efficiency and policy Recent Publications His 2023-2025 publications demonstrate a strong focus on enhancing software testing (e.g., Tyche for property-based testing), advancing formal verification tools (e.g., Coq deautomation), and pioneering sustainable computing frameworks. Climate-related research is a growing theme. Awards and Honors 2024: Distinguished Paper Award (ICSE) 2020: Best Paper Award (POPL) 2015: Most Influential Paper Award (ACM SIGPLAN) 2013: LICS Test of Time Award 2012: ACM Fellow Advising and Grants He advises 8 PhD students on topics ranging from type systems to verified compilation. Notable projects include: NSF-funded Carbon Connect expedition SHF grant for usable property-based testing Development of verification tools (VERSE, Unison) Professional Activities Serves on editorial boards for Journal of Functional Programming and Logical Methods in Computer Science , and organizes major conferences (PLDI, POPL, OOPSLA). Advocates for low-carbon virtual conferences.
Bas Testerink is a Researcher at the Faculty of Science , Utrecht University , focusing on Responsible AI . He works in the AI & Data Science subtheme with research interests in Human-centered Artificial Intelligence and Applied Data Science . Email: b.j.g.testerink@uu.nl Office: Minnaert Building, Leuvenlaan 4, Room 304, Utrecht His research explores Norm Enforcement in distributed systems, Multi-Agent System design, and Runtime Verification mechanisms. Key projects include AI-assisted message processing for police and Norm-based traffic control systems . Recent publications highlight his work on Argumentation-based Inquiry (2022) and Collaborative Monitoring (2016). He also investigates Security Threats in collaborative verification and Organizational Replication through inheritance models. He contributes to: Autonomous Vehicles regulation Crime Analysis through AI Peer-to-Peer Argumentation frameworks His work appears in venues like PRIMA , ECAI , and AAMAS .
Stefan Alexander Schupp is a researcher affiliated with the Department of Cyber-Physical Systems at Technische Universität Wien (TU Wien). His work focuses on formal verification, hybrid systems, and controller synthesis for cyber-physical systems. Department: Cyber-Physical Systems (E191-01) Research Affiliation: TU Wien Network Lab Research interests include: Hybrid and stochastic system verification Controller synthesis for real-time systems Formal methods in software engineering Design and analysis of safety-critical systems Automated model checking techniques Flowpipe construction for reachability analysis Recent publications highlight collaborations with researchers from multiple institutions, covering topics such as: Hyperproperty verification in distributed systems Metric Temporal Logic (MTL) controller synthesis Adaptive simplex architectures for bounded-liveness properties Stochastic hybrid automata analysis tools HyPro verification tool developments Probabilistic reachability optimization
Hongjin Liang is an Associate Professor at the School of Computer Science , Nanjing University , China. He is an active researcher and educator in the fields of programming languages and formal verification, with a strong focus on concurrency theory, mechanized proofs, and memory models. Education: PhD in Computer Science (May 2014), dissertation titled Refinement Verification of Concurrent Programs and Its Applications . Research Interests: His research spans formal verification , concurrent programming , memory models , and mechanized reasoning . He is particularly known for his work on verifying concurrent data structures, program logics for concurrency, and certified compilation. He is a member of the PLaX research group . Publications and Impact: Liang has published extensively in top-tier venues such as POPL, PLDI, ESOP, TOPLAS, and CSL-LICS. His work often involves formalizing and verifying complex concurrent systems using interactive theorem provers like Rocq/Coq. Notable contributions include verifying compiler optimizations under weak memory models and developing program logics for randomized concurrent programs. Scientific Awards: Distinguished Paper Award , PLDI 2019 for "Towards Certified Separate Compilation for Concurrent Programs" Teaching and Advising: He teaches undergraduate and graduate courses including Formal Semantics of Programming Languages , Concurrency: Algorithms and Theories , and Compiler Design . He has supervised graduate students and served on numerous program committees for international conferences. Affiliations: He is affiliated with the PLaX research group at Nanjing University and has collaborated with researchers such as Xinyu Feng, Zhong Shao, and Jan Hoffmann.
Benjamin C. Pierce is the Henry Salvatori Professor of Computer and Information Science in the School of Engineering and Applied Science at the University of Pennsylvania. As a Fellow of the ACM, he has made significant contributions to programming language theory and formal methods. His academic leadership includes previous editorial roles as co-Editor in Chief of the Journal of Functional Programming and Managing Editor for Logical Methods in Computer Science. His research spans multiple interconnected domains in programming language theory, with particular emphasis on type systems and their applications to security and verification. Pierce's work bridges theoretical foundations with practical implementations, most notably through his development of the Unison file synchronization tool and contributions to the Clowdr virtual conference platform. His research interests form a cohesive trajectory from foundational type theory to applied security and verification techniques. Pierce's scholarly output shows consistent focus on property-based testing, type systems, and formal verification methods. His recent publications demonstrate evolving interests in differential privacy verification, synchronization technologies, and the practical challenges of implementing formal methods in real-world systems. The progression of his work reflects both theoretical depth and practical relevance to software development challenges. Fellow of the ACM Author of influential textbooks Types and Programming Languages and Software Foundations Lead designer of the Unison file synchronizer Co-developer of the Clowdr virtual conference platform Former editorial leadership for multiple prominent programming languages journals As an educator and mentor, Pierce has contributed to the Programming Languages Mentoring Workshop (PLMW) and has served on numerous conference program committees. His academic service extends to SIGPLAN leadership roles including SIGPLAN Vice Chair and Steering Committee membership. His textbook Software Foundations has become a standard resource for teaching formal methods and proof assistants.
Tim Würtele is a Ph.D. researcher at the Institute of Information Security at the University of Stuttgart. His work focuses on formal security analysis of cryptographic protocols, particularly those underpinning critical web standards like OAuth 2.0, OpenID Connect, FAPI, ACME, and Web Payment APIs. He has contributed to identifying and mitigating vulnerabilities in these protocols, collaborating with standardization bodies such as the OpenID Foundation and W3C. University of Stuttgart Würtele's research interests include web security , cryptographic protocol verification , and formal methods for analyzing real-world implementations. His work addresses both theoretical and practical security flaws in protocols used by billions of users globally, spanning high-risk sectors like open banking and healthcare. He has published extensively in top-tier venues such as IEEE S&P, CCS, and ESORICS, often uncovering critical vulnerabilities and proposing formally verified fixes. In 2025, Würtele co-authored a paper introducing audience injection attacks , a novel class of vulnerabilities in Web-based authentication standards. His 2024 publications focused on fixing and verifying the FAPI 2.0 protocol , while 2023 papers addressed GNAP and layered protocol analysis . Earlier works (2021–2022) scrutinized the ACME certificate management standard and W3C Web Payment APIs , revealing over-charge vulnerabilities and formalizing security guarantees.
Brad Karp is a Professor of Computer Systems and Networks at University College London (UCL) , holding this position since 2005. His career spans multiple institutions and roles, including a Senior Lecturer (2005-2014) and Reader (2007-2014) at UCL, Adjunct Assistant Professor at Carnegie Mellon University , and Senior Staff Researcher at Intel Research Pittsburgh . He earned his PhD in Computer Science from Harvard University (2000) , preceded by an M.Sc. (1995) and B.Sc. (1992) in the same field from Harvard and Yale respectively. Research Interests : Systems security (operating systems, web browsers, application security) Wireless networking (multi-antenna capacity, interference management) Network routing (robustness, low-latency protocols) Distributed systems (DHTs, sensor networks) Scientific Contributions focus on optimizing network performance, enhancing security architectures, and developing practical routing algorithms. His work on gradient compression (2024) and low-latency routing topologies (2018) demonstrates continued relevance in network design. Earlier publications like OpenDHT (2005) and Polygraph (2005) established foundational contributions in distributed systems and security. Awards & Recognition : Royal Society-Wolfson Research Merit Award (2005-2010) Best Paper Award (Usenix 2014) Professional Activities include program committee roles for ACM SIGCOMM (2009, 2011-2017), HotNets (2008-2017), and NSF review panels. He has examined PhD theses at the University of Cambridge (2010) and contributed to the HotNets Steering Committee (2009-2014).
Phillip Rogaway is a Professor in the Department of Computer Science at the University of California, Davis, within the College of Engineering. His work focuses on cryptography and cybersecurity, particularly authenticated encryption, secure communication protocols, and cryptographic definitions. University: University of California, Davis Department: Computer Science Ranks: Professor Rogaway's research spans foundational and applied cryptography, including deterministic encryption, format-preserving encryption, and provable security frameworks. He actively contributes to cryptographic standards like OCB and explores the social and ethical dimensions of cryptographic work. His recent publications emphasize authenticated encryption mechanisms, secure data distribution, and cryptographic efficiency. Rogaway has received grants such as the SaTC: CORE: Small: Crypto-for-Privacy (2017) and participated in workshops like the Dagstuhl Seminar on Symmetric Cryptography (2012). Rogaway also engages in educational advocacy, authoring materials like "Giving Good Talks" (2017) and "Introduction to Modern Cryptography" (2012). His work underscores the importance of aligning cryptographic practices with societal needs.
