David Walker is a Professor at Princeton University in the Department of Computer Science . His research spans multiple areas including Programming Languages , Networking , Type Systems , and Semantics . His recent work focuses on Network Verification , Logic Programming , and Type-Theoretic Synthesis . He has contributed to conferences such as PLDI , POPL , SPLASH , and ICFP , with research trends emphasizing Formal Methods , Distributed Systems , and Language Design . Scientific Contributions: 2024 PLDI: Modular Control Plane Verification via Temporal Invariants 2023 SPLASH: SwitchLog and Saggitarius DSL 2022 PLDI: Safe Packet Pipeline Programming 2021 SPLASH: Data-Driven Invariant Inference 2020 POPL: Abstract Network Control Plane Interpretation
Joseph C. Osborn is an Associate Professor in the Department of Computer Science at Pomona College, where he has been a faculty member since 2018. He is affiliated with the FAIM Lab (Formal Analysis and Interactive Media Lab), which focuses on the intersection of AI, game design, and formal methods for interactive systems. Ph.D. in Computer Science, University of California, Santa Cruz M.F.A. in Interactive Media, University of Southern California B.S. in Software Engineering and Computer Science (Double Major), Rochester Institute of Technology (RIT) His research explores how AI and formal verification techniques can support and enhance the design of interactive systems, particularly video games. Drawing from both computer science and fine arts backgrounds, he develops novel knowledge representations to help designers understand the implications of their design choices. His work spans software model checking, machine learning, game studies, and HCI, with a focus on enabling computational systems to reason about interactivity. His recent publications reveal a strong trend in automated game analysis, procedural content generation, and formal modeling of game mechanics. He has developed tools like Mappy for automatic NES game mapping and contributed to hybrid system modeling of action games. His research integrates symbolic reasoning, dynamic analysis, and AI to support creative design processes. Best Student Paper, AIIDE 2017 Best Paper Honorable Mention, Foundations of Digital Games 2017 Outstanding TA Award 2016–2017 Best Paper Nomination, Foundations of Digital Games 2015 He advises student research through the FAIM Lab and has taught courses in AI, computational logic, software verification, and game development. His work bridges theoretical computer science with practical creative applications in interactive media.
Mohammad Izadi serves as Associate Professor at Sharif University of Technology's Department of Computer Engineering and directs the Distributed and Multiagent Systems Lab (DiSysLab). He holds dual PhDs in Computer Science from Leiden University and Computer Engineering from Sharif University of Technology. Research expertise spans: Formal analysis of distributed systems using modal/temporal logics Game-theoretic resource allocation in cloud/edge networks Natural language processing with Persian language specialization Semantics of programming languages and Reo coordination models His teaching portfolio includes graduate courses on Distributed Systems, Algorithmic Game Theory, and Logic for Computer Science. He actively supervises 6 PhD candidates and has graduated 18 master's students, with research focusing on workflow scheduling, NLP, and formal verification. Administrative leadership: Dean of Education at Sharif University (2016-2021) Vice-chairman of Iranian Society of Engineering Education
Jan Křetínský is an Assistant Professor at the Technical University of Munich (TUM) , affiliated with the TUM School of Computation, Information and Technology . His work focuses on formal methods for software reliability, including error detection, correctness proofs, and performance optimization of stochastic and real-time systems. He employs techniques from automata theory, logic, probability theory, and machine learning in his research. Education: Studied computer science, mathematics, philosophy, and linguistics at Masaryk University (Brno, Czech Republic); earned a doctorate (summa cum laude) in 2013 from Masaryk University and TUM. His research emphasizes verification and synthesis of safe controllers, with applications in probabilistic and temporal logic frameworks. Publications highlight intersections of formal methods, machine learning, and stochastic systems. Scientific Awards: IST Fellow (Institute of Science and Technology Austria)
Stephen Powell is an Associate Professor in the School of Physics and Astronomy at the University of Nottingham, where he has been a faculty member since 2013. He is a member of the Condensed Matter Theory group, focusing on theoretical condensed matter physics. 2013–present: University of Nottingham 2012–2013: Assistant Professor, Nordita 2009–2012: JQI Postdoctoral Fellow, University of Maryland, supervisor: Sankar Das Sarma 2007–2009: Postdoctoral Research Assistant, University of Oxford, supervisor: John Chalker 2002–2007: Ph.D., Yale University, adviser: Subir Sachdev 1998–2002: M.Phys., Christ Church, University of Oxford Dr. Powell's research investigates the properties of novel phases of matter, with a focus on understanding unconventional phenomena and the physical systems in which they occur. His primary approach is through the concept of frustration, which describes systems where interactions compete against one another, preventing simple ordered states from forming. Instead, strong correlations and large fluctuations can coexist, leading to exotic phases and phenomena such as "spin liquids," states characterized by topological order and the emergence of fractionalized excitations. His research spans multiple areas including spin ice systems, quantum phase transitions, dimer models, and frustrated magnetic systems. His work often combines analytical techniques with numerical simulations to explore the rich physics of these complex systems. PHYS1001: From Newton to Einstein PHYS4017: Quantum Dynamics PHYS4029: Order, Disorder and Fluctuations MPAGS SM2: Classical and Quantum Phase Transitions (Convenor) Dr. Powell's recent publications show a strong focus on spin ice systems, dimer models, and quantum phase transitions. His work often explores the connections between classical and quantum systems, with particular attention to topological properties and emergent phenomena. The research demonstrates a consistent trajectory toward understanding complex phase transitions and the unusual behavior of frustrated magnetic systems.
Cristina Sirangelo is a Professor of Computer Science at Université Paris Cité, affiliated with the Institut de Recherche en Informatique Fondamentale (IRIF) and on INRIA delegation at ENS Paris within the VALDA team. Her work bridges database theory, logic, and automata theory, focusing on query answering in incomplete data environments and XML processing. Ph.D., University of Calabria (2005) Habilitation à diriger des recherches, ENS de Cachan (2014) Her research explores computational complexity in consistent query answering, Datalog and first-order logic for XML querying, and automata-based validation. Recent projects emphasize dichotomy theorems for query complexity and algorithmic solutions for database constraints under primary keys. She has been recognized with the ICDT 2013 Test of Time Award for foundational work on XML with incomplete information. Her publications span top-tier venues like PODS, ICDT, JACM, and LMCS, with a focus on logical frameworks and efficient data processing. ICDT 2013 Test of Time Award : For pioneering work on XML with incomplete data. As a teaching leader, she co-organizes the master DATA program and the MIDS double master in data science. Her collaborative efforts include co-authoring key papers on XML reasoning, data exchange, and histogram-based data summarization.
Patricia Bouyer-Decitre is a prominent researcher at Université Paris-Saclay , where she co-leads the Laboratoire Méthodes Formelles (LMF) (CNRS, ENS Paris-Saclay). Her work bridges mathematical rigor with applied computer science, focusing on formal methods to verify safety-critical software in avionics, automotive systems, and medical devices. Education: École normale supérieure de Cachan (mathematics & computer science), LSV (thesis on time-dependent systems) Leadership: Director of LMF since 2021; former LSV leadership (2020) Her research centers on mathematical models for system verification, including timed automata and Markov processes, with applications in robotics and digital health. Key projects address uncertainty management in software through game theory-inspired frameworks. Grants: ERC grant (2013–2019, €1.5M) Awards: CNRS Bronze Medal, European Presburger Award (theoretical computer science) Collaborations span Institut des systèmes intelligents et de robotique (ISIR) , IRISA, Aalborg University, and University of Mons. She emphasizes interdisciplinary environments that translate abstract models into industry-ready solutions.
Sebti Mouelhi is a Lecturer-Researcher at ESTACA'LAB, Pôle S2ET (Systems and Embedded Energies for Transportation), ESTACA Campus Paris-Saclay, France, since 2020. Previously, he held the same role at ECE Paris (2015-2020). His academic work bridges formal verification, control systems, and cybersecurity in transportation contexts. PhD in Computer Science (Université de Franche-Comté, 2011) M.Sc. in Computer Science (University of Lorraine, 2007) His research focuses on formal verification of component-based systems, controller synthesis for hybrid systems, and cybersecurity in vehicular and IoT communications. Recent work includes behavioral contracts for railway systems and V2X waveform optimization . Publications highlight trends in autonomous vehicle security , component-based design , and transportation-specific formal methods . He has contributed to tools like CoSyMA for control synthesis and explored multi-scale abstractions in hybrid systems. Teaching activities include labs on embedded Linux , real-time scheduling , CAN bus , and FreeRTOS using STM32 microcontrollers. His industrial experience (2012-2015) complements his academic expertise with practical insights into safety assurance and R&D in transport technologies.
Professor Igor Potapov serves as a Professor of Computer Science at the University of Liverpool, leading the Algorithms, Complexity Theory and Optimisation research group and acting as Council Member for Networks Sciences & Technologies. He holds key administrative roles including Director of MSc Studies in CS with Year in Industry and module coordination for Efficient Sequential Algorithms (COMP309), MSc Industrial Project (COMP599), and MSc Placement Experience (COMP598). His research centers on theoretical computer science with emphasis on reachability problems in infinite state systems , distributed computing and pattern formation , combinatorial optimisation , and decidability questions for mathematical structures. Current interdisciplinary work includes Algorithmic Crystal Structure Prediction for Material Design (Royal Society APEX Award 2024-2026) and foundational studies in automata-matrix theory connections. His methodological approach integrates abstract algebra, topology, and computation theory to analyze computational boundaries. Recent publications (2024-2025) demonstrate strong convergence between theoretical frameworks and practical applications, particularly in robotics scheduling (addressing collision avoidance and safety verification) and mathematical decidability (matrix semigroups, linear recurrence systems). These works bridge computational geometry with distributed algorithm design, revealing novel complexity boundaries in reachability analysis. His scientific recognition includes: Royal Society Apex Award (2024-2026) for Algorithmic Crystal Structure Prediction Royal Society Leverhulme Trust Senior Research Fellowship (2020-2021) for "Cornerstones of Reachability" As an active grant recipient, he manages multiple projects including Algorithmic Intelligence for Life, Society and Science (Royal Society 2024-2026) and UoL-SumDU Collaboration for Digitalisation of Ukraine (Research England 2023-2024). He supervises thesis work on crystal structure prediction and distributed shape formation while serving on examination committees for Oxford, Leicester, and Gran Sasso institutions. He co-leads the Science for Ukraine initiative's UK branch, developing academic mentoring programs and research twinning partnerships between UK and Ukrainian universities. His editorial work spans Fundamenta Informaticae (2020-present) and Lecture Notes in Computer Science (2009-2013), alongside conference organization for the Reachability Problems series.
Frederik Ravn Klausen is a Guest Researcher at the Department of Mathematical Sciences, University of Copenhagen, and a postdoc in mathematical physics at Princeton University. His research focuses on mathematical physics, statistical mechanics, and quantum systems. His recent publications explore topics such as Anderson localization in open quantum systems, phase transitions in the Ising model, scalability challenges in analogue quantum simulators, and stochastic cellular automaton models of culture formation. Collaborative work spans interdisciplinary areas between physics, mathematics, and computational modeling.
Ning Luo is a tenure-track Assistant Professor in the Department of Electrical and Computer Engineering at the University of Illinois Urbana-Champaign. She holds a Ph.D. in Computer Science from Yale University and completed a postdoctoral fellowship at Northwestern University. Education: BS in Mathematics, Shandong University (2017); Ph.D. in Computer Science, Yale University (2022) Her research focuses on combining formal methods , automated reasoning , programming languages , and cryptography to achieve security , verifiability , and confidentiality in complex systems. Recent works include zero-knowledge proofs for SMT theorems, privacy-preserving interdomain verification, and oblivious automata for secure regular expression matching. Her publications span top venues like USENIX Security , CCS , ESORICS , and INFOCOM , with interests in zero-knowledge protocols , formal verification , secure multi-party computation , and privacy-enhancing technologies . She has received multiple awards including the Yale Distinguished Dissertation Award (2023) and CCS Distinguished Paper Award (2022). Ph.D. advisees: Gefei Tan (UIUC), Lenny Liu (UIUC) Former mentees: Haotian Chu (NU), John Kolesar (Yale), Daniel Luick (Yale) She teaches courses on Computer Security , Cryptography , and Deployable Privacy Technologies , emphasizing hands-on implementation of cryptographic frameworks like MP-SPDZ and ObliVM. Her lab (CSL 457) actively seeks students with strong research integrity.
Agostino Cortesi is a Full Professor of Computer Science at Ca' Foscari University of Venice, where he has served since 2002. He holds significant administrative roles including Rector's Delegate for Research Quality Evaluation and Deputy Coordinator of the Scientific Committee of the Temporary Innovation Ecosystem Project Center. His academic home is the Department of Environmental Sciences, Computer Science and Statistics. Dr. Cortesi received his PhD in Applied Mathematics and Informatics from the University of Padova in 1992, followed by a post-doctoral position at Brown University. His academic career has included leadership positions as Dean of the Computer Science programme, Department Chair, and Vice-Rector of Ca' Foscari University for quality assessment and institutional affairs. His research focuses on programming languages theory, software engineering, and static analysis techniques with particular emphasis on security applications. His work spans abstract interpretation, information flow analysis, string analysis for program verification, and security applications in blockchain and IoT systems. He has published extensively with over 150 papers in high-level international journals and conference proceedings, with an h-index of 22 according to Scopus and 31 according to Google Scholar. His recent publications show a consistent focus on abstract interpretation techniques applied to string analysis, security verification for blockchain and IoT systems, and tools for static analysis. His work bridges theoretical foundations with practical applications, particularly in security-critical domains. Dr. Cortesi serves on the editorial boards of Computer Languages, Systems and Structures and Journal of Universal Computer Science, and has participated in numerous program committees for international conferences including SAS, VMCAI, CSF, CISIM, and ACM SAC. He teaches several advanced courses including Software Correctness, Security, and Reliability; Data Programming; Information Networks and Systems; and Software Engineering across both Computer Science and Business Administration programs. His research is supported by multiple funded projects from the European Union, Italian Ministry of Education, Veneto Region, and industry partners.
Erika Ábrahám is a Full Professor at RWTH Aachen University , Germany, leading the Theory of Hybrid Systems research group. Her academic journey includes positions as a Junior Professor (2008-2013) and postdoctoral researcher at institutions like Jülich Research Centre and Albert-Ludwigs-University Freiburg. Her research interests span formal methods, SMT solving, hybrid systems verification, and probabilistic systems. She has contributed to symbolic computation, railway timetables, and probabilistic hyperproperties, with recent work focusing on cylindrical algebraic decomposition, conflict-driven search algorithms, and stochastic modeling. Scientific contributions include 15+ articles (2021-2025) on topics like probabilistic hyperproperties , hybrid automata , and symbolic arithmetic , often published in LNCS, Springer, and Elsevier venues. She has collaborated on tools like HyPro and SMT-RAT, and edited proceedings for conferences including NASA Formal Methods and QEST.
Loris D'Antoni is an Associate Professor in the Department of Computer Science and Engineering at the University of California at San Diego (UCSD). He also holds a visiting academic position at AWS. His research focuses on helping people write trustworthy software through advances in programming languages, program verification, and synthesis techniques. Education : Bachelor's and Master's degrees in Computer Science from the University of Torino (2008-2010); PhD in Computer Science from the University of Pennsylvania (2015). His research interests span programming languages, formal verification, program synthesis, automata theory, and trustworthy machine learning systems. Recent work includes developing frameworks for semantics-guided synthesis (SemGuS), formal verification of fairness in machine learning, and methods for constraining large language models of code. Recent publications address topics like access control policy analysis, grammar-constrained decoding for language models, and automated specification synthesis. These works intersect computer science, formal methods, and machine learning. Awarded multiple prestigious accolades including the NSF CAREER Award, Microsoft Research Faculty Fellowship, and Google Faculty Award, he has also received the Morris and Dorothy Rubinoff Dissertation Award and was a Phillip R. Certain-Gary D. Sandefur Distinguished Faculty Award recipient. D'Antoni advises PhD students including Keith Johnson, Shaan Nagy, Jinwoo Kim, and Kanghee Park. Former advisees like Yuhao Zhang, Qinheping Hu, and Kausik Subramanian have moved on to prominent roles at companies such as Amazon, Google, and Facebook. He leads the Programming Systems Group at UCSD and collaborates with AWS on specification-aligned LLMs. His work also involves tools like AutomataTutor for education and projects at the intersection of program synthesis and machine learning robustness.
Nathanaël Fijalkow is a senior researcher at CNRS in LaBRI, Bordeaux, where he leads the Synthesis team. His work bridges program synthesis, games on graphs, automata theory, and applications in machine learning and formal verification. Research interests include: Program synthesis and code generation Game theory for algorithmic verification Linear Temporal Logic learning Probabilistic automata and dynamical systems Boolean network synthesis for biological modeling Recent publications focus on GPU-accelerated program synthesis, decidable classes of POMDPs, and optimal transformations in automata theory. He received the AAAI 2025 Outstanding Paper Award. He supervises PhD students and collaborators in the Synthesis team, working on projects like ANR ZADyG, ANR Shannon meets Cray, and PEPR IA SAIF. The team develops tools such as Scarlet and BoNesis for LTL learning and Boolean network analysis.
