Ralf Bierig joined Maynooth University's Computer Science Department in 2017, teaching topics including information retrieval, software testing, interaction design, and virtual reality. He is the programme director of the Higher Diploma in Human-Computer Interaction (HCI) and User Experience (UX). He earned his BSc (2002) from University of Furtwangen and PhD (2008) from Robert Gordon University. Research Interests His work spans information retrieval, interactive information retrieval, personalisation, information search behavior, usability (UX), and virtual reality (VR). Recent publications focus on multimodal concept indexing, hybrid IR approaches, and contextual adaptation in search systems. Publication Trends His research combines statistical semantics, graph modeling, and multimodal data analysis across academic collaborations in Austria, Germany, and international venues like ECIR and SIGIR.
Zachary Kincaid is an Associate Professor in the Department of Computer Science at Princeton University's School of Engineering and Applied Science. His research focuses on program analysis, logic, and programming languages, with an emphasis on making program analysis compositional and robust. He received his PhD from the University of Toronto under the supervision of Azadeh Farzan. His work has been implemented in the Duet program analyzer, and he has an Erdős number of 3. Dr. Kincaid's research interests include: Compositional program analysis techniques Algebraic approaches to program analysis Termination analysis and ranking function synthesis Verification of concurrent and parallel programs Automated reasoning and decision procedures Analysis of numerical programs and loops His recent publications show a strong focus on developing novel techniques for program analysis that bridge theoretical computer science with practical verification tools, particularly in nonlinear analysis, quantified reasoning, and compositional verification. Dr. Kincaid has received research support from ONR grant N00014-19-1-2318 for his work on robust program analysis. He has advised graduate students including: Current: Jake Silverman, Nicolas Koh, Nikhil Pimpalkhare Graduated: Shaowei Zhu (PhD 2024, Researcher at Amazon), Charlie Murphy (PhD 2023, Postdoc at University of Wisconsin–Madison) Dr. Kincaid teaches courses including: COS 320 – Compiling Techniques (Spring 2024, 2022, 2020, 2019) COS 516 / ELE 516 – Automated Reasoning about Software (Fall 2025, 2022, 2018) COS 217 – Introduction to Programming Systems (Fall 2024) COS IW – Practical Solutions to Intractable Problems (Fall 2023, Spring 2023, 2018, 2017) COS IW – Little Languages (Spring 2018) COS 597D – Reasoning about concurrent systems (Fall 2016)
Dmitriy Traytel is an Associate Professor at the University of Copenhagen's Department of Computer Science since August 2020, where he currently heads the Software, Data, People & Society (SDPS) section. Prior to this position, he worked as a senior researcher (Oberassistent) in the Information Security Group led by David Basin at ETH Zürich. He completed his PhD at TU München under Tobias Nipkow's supervision in 2015. His research focuses on formal methods, particularly logic, automata theory, runtime verification and monitoring, decision procedures, (co)induction and (co)recursion, and interactive theorem proving. Traytel develops formally verified tools for runtime monitoring including VeriMon, TimelyMon, and WhyMon, emphasizing correctness and efficiency in monitoring complex temporal properties. His recent publications (2021-2025) demonstrate a strong focus on first-order temporal logic monitoring, with particular attention to explainable verdicts, scalable parallel implementations, and formal verification of monitoring algorithms. The work spans theoretical foundations in logic and category theory while maintaining practical applications in runtime verification systems. Distinguished Paper Award at POPL 2025 for 'Barendregt Convenes with Knaster and Tarski' Best Student Paper Award at FSCD 2016 Distinguished Paper Award at ATVA 2018 Traytel has supervised numerous PhD, Master's, and Bachelor's students in areas spanning formal verification, runtime monitoring, and theorem proving. His research has been supported through collaborations with major institutions including ETH Zürich and TU München. He actively contributes to the academic community by serving on program committees for major conferences including ITP 2025 and RV 2025. He leads the Software, Data, People & Society section at the University of Copenhagen, focusing on developing formally verified tools for runtime verification that bridge theoretical computer science with practical applications in security and system monitoring.
Tiark Rompf is an Assistant Professor at Purdue University , with research spanning programming languages, compilers, and systems. His work bridges domains including architecture, databases, machine learning, and AI through projects like Reachability Types and Rhyme. Co-director of the Purdue Center for Programming Principles and Software Systems (PurPL) Scientific Advisor at SambaNova Systems Previously a member of the Scala team at EPFL His research focuses on: Runtime code generation and advanced compiler technology Expressive data-centric query languages (Rhyme, Datalog) Reachability type systems for memory safety and effect handling Metaprogramming and logical relations for formal verification Recent publications highlight contributions to Datalog compilation (Flan), nested data structures (Rhyme), and polymorphic reachability types. He leads projects exploring: Compiler optimizations for emerging architectures (GPU, TPU, FPGA) ML-driven compiler improvements Secure multi-party computation via metaprogramming Scientific awards include: NSF CAREER Award (2016) Google Faculty Research Awards (2017, 2018) DOE Early Career Research Award (2017) ACM SIGPLAN PL Software Award (2019) GPCE Test of Time Award (2020) Students and alumni from his group have joined institutions like Databricks, DeepMind, Galois, and Meta. He teaches advanced compiler courses including: CS 590 - Advanced Topics in Compilers CS 352 - Compilers CS 502 - Graduate Compilers
Dr. Ana Milanova is a Professor in the Department of Computer Science at Rensselaer Polytechnic Institute, where she has been since 2003. Her research focuses on programming languages, compilers, and software engineering, with emphasis on static program analysis, security, and applications in Android app taint analysis, secure cryptographic protocols, and machine learning library verification. Research Interests: Her work addresses challenges in secure software development, privacy-preserving techniques, and static analysis methodologies. Recent projects include federated learning frameworks, Python-based static analysis tools, and secure computation protocols. She has contributed to tools like Submitty for automated programming assignment grading and frameworks for secure MapReduce applications. Scientific Awards: NSF CAREER Award, Google Faculty Research Award Grants: SaTC: CORE grants for secure computation and multi-party optimization Labs/Teams: Leads research in secure computation, federated learning, and static analysis tool development. Collaborates on open-source platforms for educational grading systems (Submitty).
Sylvain Conchon is a Professor at Université Paris-Saclay, affiliated with the Laboratoire Méthodes Formelles (LMF, UMR 9021) and the Toccata research team, a joint project with INRIA Saclay – Île-de-France. His work lies at the intersection of formal methods, automated reasoning, and software verification. Research Interests: His primary research areas include SMT solving, automated deduction, program verification, model checking for parameterized systems, and information flow analysis. He develops theoretical foundations and practical tools to ensure software correctness, particularly in safety-critical and concurrent systems. Publications and Tools: His recent work centers on projects like BPI IDemo ARGOS (2024) and PEPR Secureval (2022), focusing on industrial software verification and cybersecurity. He is the main developer of Alt-Ergo , an SMT-based theorem prover, and Cubicle , a model checker for parameterized systems. His publications span formal methods, logic in computer science, and static analysis, with a strong emphasis on tool building and application. Scientific Awards: Advising and Grants: He has advised several PhD students including Guillaume Girol, Alain Mebsout, and Mohamed Iguernelala. He has led and participated in numerous research projects funded by ANR, FUI, PEPR, and industrial partners, demonstrating sustained grant success in formal methods and verification. Labs and Teams: He is a core member of the Toccata team at INRIA Saclay and the LMF laboratory, where he collaborates on advancing the state-of-the-art in deductive program verification and automated reasoning.
François Pottier is a senior researcher at Inria in Paris, France, where he leads the Cambium research team. He is affiliated with the Gallium research group and has maintained an active research profile spanning several decades in programming languages and formal methods. His research focuses on programming languages , particularly functional programming and OCaml, type systems design and implementation, program verification using separation logic, and compiler construction . His work bridges theoretical foundations with practical implementation, evidenced by numerous open-source software tools he has developed. Pottier's publication record shows consistent contributions to top programming languages conferences (POPL, ICFP, ESOP) with recent work emphasizing separation logic frameworks, resource analysis, and formal verification of OCaml systems. His research demonstrates a clear trajectory from foundational type theory toward practical verification techniques for real-world programming languages. He has advised numerous PhD students including Remy Seassau, Tiago Soares, Clément Allain, and Alexandre Moine, among others, many of whom have gone on to research positions at institutions like New York University, Imperial College London, and Inria itself. Pottier maintains active service roles in the programming languages community as a member of IFIP Working Group 2.8 on Functional Programming and IFIP Working Group 2.16 on Language Design, and serves on program committees for major conferences including upcoming roles for JFLA 2026 and ITP 2026. He leads the Cambium research team at Inria, which focuses on programming language theory and implementation, particularly around OCaml and formal verification. The team develops both theoretical frameworks and practical tools that have influenced the broader programming languages ecosystem.
Anders Møller is a Professor and Vice Head of Department at the Department of Computer Science, Aarhus University, Denmark. He is a leading researcher in programming languages and software engineering, with a primary focus on static and dynamic program analysis. He serves as Chairman of the PhD Committee and holds leadership roles in the international research community, including Vice-Chair of ACM SIGPLAN and Associate Editor for ACM TOPLAS and ACM TOSEM. His research interests include programming languages, software engineering, static and dynamic analysis, program verification, and security. His work bridges theoretical foundations and practical applications, particularly in improving software reliability and security through advanced analysis techniques. The trends in his recent publications reflect a strong emphasis on static analysis for security, scalability, and real-world impact—especially in web applications, smart contracts, and open-source software supply chains. His research has evolved toward practical deployment, demonstrated by the founding and acquisition of Coana by Socket in 2025 for enhanced vulnerability detection. Recipient of the Danish Elite Research Prize 2020 ACM Distinguished Member He actively mentors students and contributes to the academic community through conference leadership (e.g., OOPSLA, PLDI, ICSE). He also co-authored the widely used textbook Static Program Analysis with Michael I. Schwartzbach. His work is deeply integrated into both academic and industrial advancements in software analysis and security.
Mohamed Faouzi Atig is a Professor in Computer Systems at the Department of Information Technology, Uppsala University. His career spans roles as Senior Lecturer (2018-2021), Associate Senior Lecturer (2014-2018), and Researcher (2012-2018) at the same institution. He obtained his Doctoral Degree in Computer Science from the University of Paris Diderot-Paris 7 (2010) and a Master in Engineering from Tunisia Polytechnic School (2005). Current Role: Professor in Computer Systems Institution: Uppsala University Research Focus: Model checking, verification of infinite-state systems, weak memory models, automata theory, string constraints, concurrent program analysis His research explores formal methods for concurrent programs, weak memory models (TSO/PSO/POWER), automata theory for verification, and SMT solvers for string constraints. Recent work integrates graph neural networks with word equation solving and advances stateless model checking techniques. Key article trends include Weak Memory Model Verification (TSO, PSO, POWER) Stateless Model Checking Algorithms String Constraint Solvers (TRAU, Norn) Timed Automata and Multi-Pushdown Systems Mohamed Faouzi Atig has led collaborations on fence insertion procedures, timed pushdown automata, and database-driven system verification. His contributions are recognized through publications in top-tier conferences and journals.
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. He earned his Ph.D. in Computer Science and Engineering from The Chinese University of Hong Kong (2013) and bachelor's degree in Computer Science from Zhejiang University (2009). Zhang teaches graduate courses in compilers, software analysis, and program analysis, including CS 6340 Software Analysis and Test (Fall 2024) and CS 4240 Compilers and Interpreters (Spring 2025). His research focuses on improving software reliability and security through program analysis and compiler optimization techniques. Key research areas include computational complexity, analytic combinatorics, graph theory, and formal languages. Current projects include SLOT (SMT-LLVM Optimizing Translation) , Mutual Refinements of Context-Free Language Reachability , and Context-Free Language Reachability with Transitive Redundancy Elimination , among others. Zhang's research has produced award-winning work including the SIGSOFT Distinguished Paper Award (FSE 2023) and PLDI Distinguished Paper Award (2020). He has advised multiple students including Ph.D. graduates Shuo Ding (2024) and Yuanbo Li (now at Facebook), with Benjamin Mikek and Camille Bossut currently pursuing their Ph.D.s. As an academic leader, Zhang has served as: Artifacts Chair: PLDI'26, PLDI'25 Program Committee: PLDI'26, POPL'26, SAS'25, ASPLOS'25, SAS'24, FSE'24 External Reviewer: PLDI'19, PLDI'18 His group maintains active GitHub repositories for tools like Perses (syntax-guided program reduction) and Skeletal Program Enumeration (compiler testing framework). Zhang also contributes to educational resources by maintaining course materials on static analysis, symbolic execution, and webassembly analysis.
Karlheinz Friedberger is a researcher at Ludwig Maximilian University of Munich's Department of Computer Science. His work focuses on formal methods, software verification, and program analysis. He has contributed to tools like CPAchecker, JavaSMT, BenchExec, and VerifierCloud, and has participated in software verification competitions. Education : PhD in Computer Science (Ludwig Maximilian University of Munich, 2021). Research Interests : Formal verification techniques, program analysis, BDD libraries, SMT solvers, and multi-threaded program validation. He has won a gold medal in Reachability Plain and a silver medal in Reachability Arithmetic at the RERS Challenge 2016. His recent publications emphasize domain-independent interprocedural analysis and tool development for formal verification.
Katalin Oláh is an Assistant Professor in the Department of Cognitive Psychology at Eötvös Loránd University (ELTE). She holds affiliations with the Institute of Psychology, Social Minds Research Group, and serves on the Research Transparency Committee. Her research focuses on developmental psychology, social learning mechanisms in children, comparative psychology (particularly dog cognition), and attention allocation strategies across ages. Key areas include linguistic in-group effects on learning, object function generalization, and emotional contagion in animals. She is reachable at olah.katalin@ppk.elte.hu and located at Izabella u. 46, Budapest. Education details: While not explicitly listed, her academic work spans developmental and comparative psychology. Doctoral data sheets are accessible via doktori.hu. Research interests emphasize social categorization formation in young children, cross-species communication, and observational learning strategies. Her publications explore topics like scale error phenomena, attention modulation by social cues, and cognitive task performance changes in dogs. Notably listed as on permanent leave from her teaching duties, though active in research and committee work.
Aleks Nanevski is a Research Professor at the IMDEA Software Institute in Madrid, Spain. He holds a Ph.D. in Computer Science from Carnegie Mellon University (2004) and completed postdoctoral research at Harvard University and Microsoft Research. His research focuses on programming languages and formal verification, particularly integrating dependent type systems with imperative features like concurrency and pointers. He co-leads the Functional Concurrent Separation Logic (FCSL) project, advancing verification techniques for concurrent programs. Education & Affiliations: Ph.D. in Computer Science, Carnegie Mellon University (2004) Postdoctoral Fellowships: Harvard University (USA), Microsoft Research (UK) Joined IMDEA Software Institute in 2009 Research Interests: Nanevski designs languages and logics that unify programming with formal verification, leveraging type theory to ensure correctness in systems with imperative features. His work emphasizes concurrency, pointer arithmetic, and modular reasoning in concurrent separation logics. Recent efforts include declarative linearizability proofs and contextual modal types for algebraic effects. Professional Activities: Program Chair: HOPE 2017, LOLA 2012 PC Member: OOPSLA 2024, POPL 2023, and multiple top-tier conferences Advising & Team: Current advisees: Jesús Domínguez, Joakim Öhman Former advisees include Ilya Sergey (Postdoc), Germán Delbianco (PhD), and Nikita Zyuzin Labs/Teams: Leads the FCSL project , developing tools for verifying fine-grained concurrent programs using dependent types and separation logic.
Adrien Pommellet is an Associate Professor at EPITA , affiliated with the Laboratoire de Recherche en Informatique (LRE) automata team. His research focuses on formal methods, automata theory, and program synthesis. Education: PhD in Computer Science from Université Paris-Diderot (2018), Parisian Master of Research in Computer Science (2012) His research interests include active and passive learning of automata , model-checking algorithms for Büchi automata, and program synthesis . He actively contributes to the development of the Spot formal verification tool. Recent publications emphasize synthesis algorithms , automata reduction techniques , and LTL verification . He has also explored type systems and formal verification of concurrent programs. Teaching roles include courses in computer science (AAA, COMP, CPXA) and formal logic (FOLO, LOFO). Formerly taught ALGO, LOGI, and PING. He worked as a research engineer at CS Communications & Systèmes before joining EPITA's LRDE (now LRE) verification team in 2019.
Tachio Terauchi is a Professor in the Department of Computer Science and Engineering at Waseda University, Japan. Previously, he held academic positions at JAIST (Professor, 2014-2017), Nagoya University (Associate Professor, 2011-2014), and Tohoku University (Assistant Professor, 2007-2011). He actively participates in program committees for premier conferences including POPL, PLDI, and SPLASH, with current service for SPLASH 2025 and POPL 2025. His academic background: B.S. in Computer Science, Columbia University (2000) M.S. in Computer Science, University of California, Berkeley (2004) Ph.D. in Computer Science, University of California, Berkeley (2006) Terauchi's research centers on techniques for building reliable computational systems through programming languages and formal methods. His core contributions span program verification for higher-order functional programs, security analysis of timing channels and regex vulnerabilities, and refinement type systems. Recent work demonstrates particular expertise in regular expressions with backreferences and temporal logic verification. His publications from 2020-2025 reveal a dominant focus on regular expression security (ReDoS vulnerabilities and repair methods) and advanced program verification techniques. This work bridges theoretical foundations in automata theory and mathematical logic with practical security applications, showing increasing specialization in regex analysis since 2022 while maintaining contributions to verification frameworks. Scientific Awards: None explicitly mentioned in the provided text. He currently advises a substantial cohort of students across all academic levels at Waseda University, with his lab actively recruiting prospective students. The lab, located in room 209B of Building 62W, supports research in programming languages and security verification through regular appointments. PhD Students: Tianrui Chen (D2), Taisei Nogami (D1) Master's Students: Kazuma Kawahara (M2), Yuta Uchijo (M2), Naoya Anada (M2), Yuki Nakayama (M1), Taisei Iida (M1) Bachelor's Students: Riru Oda (B4), Riku Ito (B4), Haruto Ishiyama (B4), Rei Tomori (B3), Rio Onoda (B3) Visiting Scholar: Nariyoshi Chida
