André Platzer is an Alexander von Humboldt Professor at the Karlsruhe Institute of Technology (KIT), where he leads the Institute for Reliability of Autonomous Dynamical Systems . He previously founded the Logical Systems Lab at Carnegie Mellon University (CMU) and held full professorships there from 2008 to 2022. His work focuses on developing logics for cyber-physical systems (CPS) to ensure safety-critical interactions between computers and physical processes. Education Ph.D. in Computer Science, University of Oldenburg (2008) Diploma (M.Sc.) in Computer Science and Mathematics, Karlsruhe Institute of Technology (2004) Research interests include Logic of Dynamical Systems , Differential Dynamic Logic , and Formal Methods . His groundbreaking work on CPS verification has led to the development of tools like KeYmaera X , applied in transportation and medical robotics. He has pioneered logics for hybrid systems, games, and stochastic processes. Scientific Awards Alexander von Humboldt Professorship for AI (2023) NSF CAREER Award (2011) IEEE Intelligent Systems' AI's 10 to Watch (2010) ACM Doctoral Dissertation Honorable Mention (2009) Popular Science's Brilliant 10 (2009) Best Paper Awards at TABLEAUX 2007, FM 2009, FM 2019, and HSCC 2022 Labs & Teams : Founded the Logical Systems Lab at CMU and leads the Institute for Reliability of Autonomous Dynamical Systems at KIT.
Benjamin Gregoire is a Researcher at INRIA Sophia Antipolis , affiliated with the Marelle Team . His work focuses on compilers , formal verification , cryptography , proof assistants , and type theory . Education : PhD in Computer Science, Université Paris 7 (2003) Research Interests : Dr. Gregoire specializes in formal verification of cryptographic systems, compiler design for security-critical applications, type-based termination, and proof assistants like Coq. His projects include the INRIA-Microsoft Research Joint Lab , ANR Scalp (Security of Cryptographic Algorithms with Probabilities), and ANR DeCert (Certified Decision Procedures). He led the Mobius project (IP FET) and contributed to Java security validation via the JACK tool . Scientific Awards : He received the Best Paper Award at CRYPTO 2011 for 'Computer-Aided Security Proofs for the Working Cryptographer.' Advising & Collaborations : Dr. Gregoire has advised PhD students Michael Armand , Julien Charles , Sylvain Heraud , and Jorge-Luis Sacchini , with former advisee Cesar Kunz . He collaborates with teams including Marelle and INRIA-Microsoft Research .
Christine Rizkallah is a Senior Lecturer in the School of Computing and Information Systems at the University of Melbourne, Australia. She joined the university in December 2021 after serving as a Lecturer at the University of New South Wales (UNSW) from April 2018 to December 2021. Her research focuses on interactive theorem proving, formal verification, programming languages, and systems, with an emphasis on building practical tools for high-assurance software development. She leads a research group working on the Cogent and Dargent languages, aiming to reduce the burden of formal verification in systems programming. Education: PhD in Computer Science, Universität des Saarlandes and Max-Planck-Institut für Informatik, Germany (2015), thesis: Verification of Program Computations , supervised by Prof. Dr. Kurt Mehlhorn. MSc in Computer Science, Universität des Saarlandes, Germany (2009), thesis: Proof Representations for Higher Order Logic , supervised by Prof. Dr. Gert Smolka and Dr. Chad E. Brown. BSc in Computer Science, German University in Cairo, Egypt (2007), thesis: X2-Planner: A Hierarchical Task Network Planner for Real Time Gaming Applications , supervised by Prof. Dr. Slim Abdennadher and Dr. Thorsten Maier. Her research interests lie at the intersection of programming languages and formal methods. She develops domain-specific languages with strong type systems and verified compilers to enable trustworthy software systems. Her work spans algorithms, logic, security, and social choice theory, reflecting a strong interdisciplinary approach. She has published extensively in top venues such as POPL, ICFP, ASPLOS, JAR, and PACMPL, with a focus on certifying compilation, refinement verification, and mechanized reasoning. Her recent publications reveal a consistent focus on formal verification of systems software, particularly through the Cogent language and its ecosystem. Key themes include verified data layout refinement (Dargent), property-based testing, termination analysis, cost modeling, and integration with foreign functions. Her work combines theoretical rigor with practical implementation, often involving mechanized proofs in Isabelle/HOL and Coq. Scientific Awards and Recognition: Distinguished Artefact Award at SLE'22 (awarded to Zilin Chen for work under her supervision). First Prize, SPLASH'22 Student Research Competition (undergraduate), won by Raphael Douglas Giles. Second Prize, ACM-wide Student Research Competition (undergraduate, 2023), won by Raphael Douglas Giles. She has supervised numerous PhD, Masters, and Honours students, many of whom have continued in academia or industry research roles. She has received research funding through institutional support and collaborative grants, though specific grants are not detailed in the provided text. She is actively involved in the programming languages community, serving on program committees for POPL, ICFP, CPP, PLDI, and others, and holding leadership roles such as Program Chair for FUNARCH'25 and Diversity and Inclusion Co-Chair for PLDI'25. She teaches core courses including Declarative Programming and Models of Computation at the University of Melbourne. She leads a vibrant research team and collaborates widely across institutions including UNSW, University of Pennsylvania, and international partners. Her lab focuses on building verified systems using functional programming and formal methods, with strong ties to the DeepSpec project and the Isabelle/HOL community.
Laure Gonnord is a Full Professor in Computer Science at Grenoble INP , affiliated with the Esisar Engineer School in Valence, France, since September 2021. She is a member of the CTSYS research team at the LCIS laboratory and an external member of the CASH team at the University of Lyon / CNRS / LIP / Inria. Her research focuses on compilation , static analysis , and applications to safety , security in high-performance and embedded systems . Fields of Interest : Compiler Design Static Analysis for Safety & Security Abstract Interpretation Embedded Systems High-Performance Programming Hardware Security Engineering Research Trends (from recent publications): Her work explores modular verification through monadic abstract interpreters, complexity bounds in term rewriting , and educational tools for theorem proving . Notable contributions include compiler hardening schemes for hardware security and memory layout optimizations for algebraic data types. Academic Leadership : Scientific Director of the Summer School EJCP (École Jeune Compilation et Programmation) Board Member of the French national research group GDR GPL Teaching Responsibilities at Grenoble INP include courses in architecture , compilation , programming languages , algorithms , and databases . She has also taught at University of Lyon, ENS Lyon, Polytech'Lille, and INSA.
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.
Michael Eichberg is a Professor at Technische Universität Darmstadt, Germany, where his work centers on software engineering, static analysis, programming languages, and secure software development tools. He is the principal architect of the OPAL framework for Java bytecode analysis and has an extensive publication record spanning PLDI, ICSE, ESEC/FSE, ISSTA, ASE, FSE, SOAP, and other premier venues. Research Interests: Static program analysis and its scalability to real-world code bases Software security, particularly cryptographic API misuse and Android app repackaging detection Concurrent and parallel programming models, including deterministic concurrency in Scala Software architecture conformance, drift and erosion detection, and rule reuse Development of open extensible tools and frameworks (OPAL, LectureDoc, QScope, Sextant, XIRC, IRC) Publication Trends: His recent work (2015-2022) demonstrates a strong focus on empirical evaluation of static analysis techniques, modular composition of analyses, and security-related program understanding. Key themes include unsoundness in call graph construction, purity and immutability analyses, parallelization of static analyses, and large-scale studies of cryptographic API misuse. Tools & Frameworks: OPAL – A flexible Java bytecode analysis and manipulation framework (core developer until 2019) LectureDoc 2 – Web-based lecture material authoring and presentation system QScope – Open extensible metrics framework for modern software projects Sextant – Eclipse-integrated software exploration tool XIRC/IRC – Frameworks for enforcing system-wide properties and architectural constraints
Beatrice Markhoff is a Professor of Computer Science (CNU 27) at the University of Tours , affiliated with the Faculty of Science and Technology (Blois site) and the Computer Science Department . She is a member of the UMR CNRS 7324 - CITERES - Archaeology and Territories Laboratory (CITERES-LAT) and the Maison des Sciences de l'Homme Val de Loire (MSH VdL) . Her research focuses on semantic interoperability , Web of data , knowledge representation , and knowledge extraction , with significant collaborations in cultural heritage disciplines . Doctorate in Computer Science, University of Franche-Comté (1995) HDR (Habilitation to Direct Research), François Rabelais University of Tours (2013) Her research themes include semantic interoperability, knowledge engineering, and data mining, with applications in cultural heritage. She co-created the International Workshop on Semantic Web for Cultural Heritage and co-edited special issues for the Semantic Web Journal and JOCCH . She leads projects like ANR SESAMES (2018-2023), H2020 ARIADNEplus (2019-2022), and H2020 4CH (2021-2023). Her academic contributions span XML data management, semantic web technologies, and functional programming. Key projects include carto4CH for cultural heritage mapping and OpenArchaeo for knowledge graph profiling. She has co-supervised PhD theses on topics like LOD querying and knowledge extraction from Wikidata .
Munindar P. Singh is the SAS Institute Distinguished Professor of Computer Science at North Carolina State University . He serves as a core faculty member in the Science of Security Lablet and contributes to initiatives in responsible computing and ethical AI . His research spans artificial intelligence , software engineering , and computing ethics . Education: Ph.D. in Computer Sciences from University of Texas at Austin (1993) B.Tech. in Computer Science and Engineering from Indian Institute of Technology, Delhi (1986) Research Focus: Dr. Singh's work centers on trustworthy AI and sociotechnical systems , with key contributions in Multiagent systems and BDI architectures Defensive cyberdeception using hypergame theory Normative systems for blockchain applications Equitable transportation systems via AI Service-oriented computing and protocol engineering Scientific Recognition: Fellow of AAAI , IEEE , and ACM Recipient of NSF CAREER Award and multiple industry awards Editor-in-Chief of ACM Transactions on Internet Technology Grant Activities: Currently leading several major NSF-funded projects including: SCC: Serving Households in Food Insecurity ($2.018M) RI: Foundations of Ethics for Multiagent Systems ($500K) Science of Security Lablet ($3.65M)
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.
Michael H. Borkowski is an Assistant Teaching Professor in the Department of Computer Science at Purdue University. He earned his Ph.D. from the University of California, San Diego (UCSD), specializing in software verification, type theory, and interactive theorem provers. His research focuses on developing techniques to ensure software correctness and performance through formal methods. Ph.D., UCSD Computer Science (2024) M.S., UCSD Computer Science (2019) B.A., Amherst College Computer Science (2016) His research interests include refinement types, functional programming, and mechanizing proofs. Recent work emphasizes software verification tools (e.g., the 2024 POPL publication on refinement types). Earlier contributions span plant biology and applied mathematics, including studies on auxin gradients and wood grain modeling. Notable awards include the Computer Science Prize and Phi Beta Kappa from Amherst College. Teaching roles include courses at UCSD (e.g., CSE 20 Discrete Mathematics) and Purdue. He was affiliated with UCSD’s ProgSys Group during his Ph.D.
Professor David J. Pym holds the position of Professor of Information, Logic, and Security at University College London's Department of Computer Science. He is also an affiliated faculty member in the Department of Philosophy and serves as Head of the Programming Principles, Logic, and Verification Group. His roles include Director of UCL's Centre for Doctoral Training in Cybersecurity, and Honorary Research Fellow jointly directing the Centre for Logic, Language, and Information (CeLLi) at the Institute of Philosophy, School of Advanced Study, University of London. Education includes a ScD from the University of Cambridge and a PhD from the University of Edinburgh. His research spans proof-theoretic semantics, reductive logic, security economics, and systems modeling. He leads major grants such as the EPSRC-funded IRIS Programme and the Leverhulme Trust grant on proof-theoretic semantics. His awards include fellowships from the Royal Society of Arts and the Alan Turing Institute. Key publications include foundational work on reductive logic and proof-search, bunched logics, and cybersecurity modeling. He advises on policy matters for the UK government and contributes to interdisciplinary education initiatives in philosophy and computer science.
Joel Chan is an Affiliate Assistant Professor in the Department of Computer Science at the University of Maryland, specializing in human-computer interaction and artificial intelligence research with applications in scholarly communication and design innovation. His work bridges computational systems and human cognitive processes to enhance knowledge work. His research portfolio emphasizes: Scholarly sensemaking and knowledge synthesis infrastructure Generative AI for hypothesis exploration and analogical reasoning Cross-disciplinary translation tools using computational linguistics Biologically inspired design systems and creativity support Human-AI collaboration in visual data analysis and programming Recent publications (2023-2025) demonstrate a decisive shift toward integrating large language models into scholarly workflows, particularly for structured hypothesis exploration and cross-domain analogical inspiration. His systems like CausalMapper and AnalogiLead exemplify practical implementations that transform theoretical frameworks into usable tools for researchers and designers. Building on foundational work in analogical innovation (2010-2022), Chan's research trajectory shows consistent evolution from studying example-based problem-solving to developing AI-augmented environments that mitigate cognitive limitations in complex knowledge tasks, with significant implications for academic practice and creative industries.
Robby is a Professor in the Department of Computer Science at Kansas State University's College of Engineering, holding the Don and Linda Glaser - Carl and Mary Ice Keystone Research Scholar title. He maintains an active research profile through the SAnToS Lab and has been continuously affiliated with the university since 2004. His educational background includes: Ph.D. in Computer Science from Kansas State University (2004) M.S. in Computer Science from Kansas State University (2000) B.S. in Computer Science from Oklahoma State University (1998) Robby's research centers on formal methods and software engineering , specializing in specification and verification techniques for high-assurance systems. His work develops user-friendly formal languages and cost-efficient verification algorithms that significantly enhance software trustworthiness in safety-critical domains like aerospace and defense systems. This research bridges theoretical foundations with practical industrial applications through tools like the Sireum framework. His publication record (2021-2025) reveals a strong trajectory toward integrated verification ecosystems, particularly the Sireum suite (Logika, Slang) and HAMR toolset for AADL-based development. These works consistently address model-code verification gaps and contract-based testing in cyber-physical systems, demonstrating growing industry adoption through collaborations with organizations like Galois and NASA. Notable recognitions include: NASA Turning Goals into Reality award (2003) NSF CAREER award (2007) ICSE Most Influential Paper award (2000) ACM SIGSOFT Impact award (2010) FMICS Best Tool Paper Award (2024) Robby's research program combines significant funding from sources like the NSF CAREER grant with active industry partnerships. His SAnToS Lab serves as a hub for developing verification methodologies that scale from academic prototypes to real-world deployment in safety-critical systems, emphasizing practical toolchains for assurance engineering. He leads the SAnToS Lab (Software Analysis and Test Organization), which focuses on advancing formal verification techniques for high-integrity software through frameworks like Sireum and HAMR, with applications spanning microkernels, cyber-physical systems, and educational tools.
Nikolaos S. Papaspyrou is a Professor at the School of Electrical and Computer Engineering of the National Technical University of Athens (NTUA), affiliated with the Software Engineering Laboratory and the Division of Computer Science. His research focuses on programming languages, compilers, formal verification, and concurrency. Since October 2021, he has been on leave from NTUA while working as a Software Engineer at Google's V8 JavaScript and WebAssembly engine team. Previously, he served as Director of the Division of Computer Science (2017–2019) and held a sabbatical at Google's Munich compiler group (2015–2016). His academic contributions include pioneering work on Erlang/OTP scalability, concolic testing for functional languages, and static analysis techniques. He has authored numerous publications in top venues like ACM Transactions on Programming Languages and Systems and IEEE conferences. Papaspyrou has supervised over 50 diploma students and multiple PhD candidates, contributing to the education of future researchers and engineers. He actively participates in programming competitions, coaching Greek Olympiad teams, and volunteers in the Hellenic Informatics Society. He teaches advanced courses on programming languages, compilers, and software engineering at NTUA, emphasizing practical applications of theoretical concepts. His educational philosophy integrates problem-solving through programming, as highlighted in his FedCSIS 2013 paper on teaching methodologies.
Anna Pappa is an Emmy Noether Group Leader at the Electrical Engineering and Computer Science Department of Technical University Berlin, leading the Quantum Communication and Cryptography group funded by DFG since 2020. Previously, she held Marie Sklodowska-Curie Fellowships at the Dahlem Center for Complex Quantum Systems (Freie Universität Berlin) and University College London (UCL). Her research focuses on quantum protocols with provable security in realistic environments, quantum communication, cryptography, and secure multi-party computation. She has a PhD from Télécom Paristech and Paris Diderot, and earlier degrees from the National Technical University of Athens (NTUA). Key achievements include experimental plug-and-play quantum coin flipping, quantum network routing algorithms, and entanglement verification techniques resistant to dishonest participants. She has received notable awards such as the Emmy Noether Fellowship (DFG) and Google Anita Borg Memorial Scholarship. Pappa’s work bridges theoretical quantum computing with practical implementations, emphasizing security in quantum systems. Her academic career includes postdoctoral roles at the University of Edinburgh and UCL, alongside software engineering experience at Nokia-Siemens Networks. She has organized seminars on cryptography and quantum computing, and her teaching spans programming languages and cryptography courses at NTUA. Pappa actively participates in conferences like QPL, QCRYPT, and AQIS, contributing to both theoretical advancements and experimental validations in quantum information science.
