**Andrei Sipoș**

*Executive Board*

**Andrei Sipoș** is a lecturer of Computer Science at the University of Bucharest and a researcher at the Institute of Mathematics of the Romanian Academy. Before that, he completed his PhD at the University of Bucharest and a three-year postdoc at TU Darmstadt. He works in the field of *proof mining*, an applied subfield of mathematical logic that aims to analyse ordinary mathematical proofs in order to obtain additional information which is not immediately apparent.

**Laurențiu Leuștean**

*Executive Board*

Laurenţiu Leuştean is a Full Professor in the Department of Computer Science, Faculty of Mathematics and Computer Science of the University of Bucharest, where he leads the Research Center for Logic, Optimization and Security (LOS). He is also a senior researcher at the Simion Stoilow Institute of Mathematics of the Romanian Academy (IMAR). His main research interests lie in proof mining, an area of applied proof theory concerned with the extraction of hidden finitary and combinatorial content from mathematical proofs. He is also interested in many-valued logics, automated theorem proving, and logic in computer science. He completed his PhD in mathematics in 2004 at the University of Bucharest under the supervision of George Georgescu. Between 2004 and 2009 he was an assistant professor and a member of the research group of Ulrich Kohlenbach in the Department of Mathematics of TU Darmstadt. In 2009 he got his Habilitation in mathematics from TU Darmstadt. Laurenţiu Leuştean received the 2010 Simion Stoilow Prize of the Romanian Academy (awarded in 2012).

**Traian Șerbănuță**

*Executive Board*

**Traian Șerbănuță** is an Associate Professor of Computer Science at the University of Bucharest, interested in programming languages, formal methods, and logics.

Traian completed his PhD at the University of Illinois, under the supervision of Grigore Roșu. He is also a research consultant for Runtime Verification, Inc., a formal-methods-based startup using technologies developed during Traian’s PhD to improve the quality of systems in industry.

**Mircea Dumitru**

*Honorary Member*

**Mircea Dumitru**, Dr. Dr. h. c. mult., is a Professor of Philosophy at the University of Bucharest since 2004. Vice-president of the Romanian Academy since 2022. Fellow of the Romanian Academy since 2021. Fellow of Academia Europaea since 2019). Rector of the University of Bucharest (2011-2019). President of the European Society of Analytic Philosophy (2011 – 2014). President of the International Institute of Philosophy (2017 – 2021). Minister of Education and Scientific Research (July 2016 – January 2017). Main publications: *Metaphysics, Modality, and Meaning. Themes from the Work of Kit Fine* (ed.) (Oxford University Press, 2020).

**Dorel Lucanu**

*Honorary Member*

**Dorel Lucanu** is a full professor at the Faculty of Computer Science, Alexandru Ioan Cuza University of Iași, Romania, where he founded and is leading the Formal Methods in Software Engineering research group. His research interests lie within the area of formal methods applied in software engineering, with a focus on logic for programs (rewriting logic, matching logic), (circular) coinductive reasoning, program verification, and program analysis (including malware analysis).

**Grigore Roșu**

*Honorary Member*

**Grigore Roșu** is a Computer Science professor at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the CEO of Runtime Verification Inc. Previously, he was a scientist at NASA, where he coined the term *runtime verification* together with his colleagues. He is interested in programming languages, formal methods, and software engineering, and especially in combining these to increase the safety, security, and dependability of computing systems. He was offered the NSF CAREER award, the UIUC outstanding junior award, the Dean’s award for excellence in research, and several best paper awards. Grigore received his PhD from the University of California at San Diego under the supervision of Joseph Goguen.

**Andrei Pătrașcu**

*Research Collaborator*

**Andrei Pătrașcu** is an Associate Professor in the Department of Computer Science of the University of Bucharest. His main research interests are computational optimization, numerical algorithms, machine learning and anomaly detection. He completed his PhD at the Politehnica University of Bucharest and recently he analysed and developed deterministic and stochastic first-order algorithms for large-scale machine learning applications.

**Marian Călborean**

*Industry Advisor*

**Marian Călborean** is an innovative entrepreneur with more than 15 years of experience in the IT Software business, with a strong technical background. An assistant professor at the University of Bucharest, in his PhD Thesis (written under the supervision of Mircea Dumitru) he developed a classical first-order treatment for vagueness. His research interests include philosophy of language, logic and computer software.

**Antonio Di Nola**

*Honorary Member*

**Antonio Di Nola** is currently an honorary professor of the Department of Mathematics of the University of Salerno. He was Mathematical Logic professor and Director of the Department of Mathematics of the University of Salerno. Since the 1990s, he has been a leading proponent of the study of algebraic models of Łukasiewicz logic (MV-algebras), the most important among the many-valued logics. His contributions to the study of MV-algebras include: a functional representation theorem for MV-algebras (aka Di Nola’s Representation Theorem); the categorical equivalences between categories of MV-algebras and categories of groups, rings, and semirings, profitably used in the literature of MV-algebras; an equational axiomatization of all varieties of MV-algebras; and a normal form theorem for Łukasiewicz logic. He introduced the class of Riesz MV-algebras, opening the study of connecting many-valued logic and Riesz spaces.

Antonio has published more than 200 scientific works and is the co-author of the monograph *Fuzzy Relation Equations and Their Applications to Knowledge Engineering*.

He is the editor-in-chief of the journal *Soft Computing*, and an associate editor to various journals. In 2013, Antonio received the IFSA Fellowship, conferred to people who have made outstanding contributions to the field of fuzzy sets and related disciplines.

**Mircea Marin**

*Research Collaborator*

**Mircea Marin** is a professor in the Department of Computer Science of the West University of Timișoara. His research interests include various aspects of declarative programming, constraint solving, unification, rewriting, formal languages, security, automated deduction and reasoning with incomplete information.

Mircea completed his PhD at the Johannes Kepler University of Linz and a postdoc at the University of Tsukuba, where he focused on the design and implementation of computational models for functional logic programming and distributed constraint solving.

**Horațiu Cheval**

*Associated Researcher*

**Horațiu Cheval** is a teaching assistant at the Faculty of Mathematics and Computer Science of the University of Bucharest and a PhD student in mathematics supervised by Laurențiu Leuștean. His main research interest is proof mining, a research program concerned with applying proof-theoretic techniques in order to extract finitary content from nonconstructive mathematical proofs. He is also interested in type theory and interactive theorem proving, his proof assistant of choice being Lean.

**Paul Irofti**

*Executive Board*

**Paul Irofti** is an Associate Professor within the Department of Computer Science of the Faculty of Mathematics and Computer Science at the University of Bucharest where he co-founded the Research Center for Logic, Optimization and Security. He is the author of book *Dictionary Learning Algorithms and Applications* (Springer, 2018, with Bogdan Dumitrescu) that was awarded the Grigore Moisil prize by the Romanian Academy. He completed his PhD in Systems Engineering at the Politehnica University of Bucharest in 2016. His main research interests are anomaly detection, signal processing, numerical algorithms and optimization.

**Doina Caragea**

*Research Collaborator*

**Doina Caragea** is a Professor at Kansas State University. Her research and teaching interests lie in the areas of machine learning, data mining, data science, information retrieval and text mining, with applications to crisis informatics, security informatics, and bioinformatics. Her projects build upon close collaborations with social scientists, security experts and life scientists, and aim to provide practical computational approaches to address real-world challenges. Dr. Caragea received her PhD in Computer Science from Iowa State University in August 2004, and was honored with the Iowa State University Research Excellence Award for her work. She has published more than 100 refereed conference and journal articles. Her research has been supported by several NSF grants.

**Bogdan Macovei**

*Associated Researcher*

**Bogdan Macovei** is a PhD student at the University of Bucharest and a teaching assistant in the Department of Computer Science, University of Bucharest. His main research interests lie within Logic and Computer Architecture.

**Vlad Rusu**

*Research Collaborator*

**Vlad Rusu** is a researcher at Inria Lille, France. Before that, he obtained his PhD at the University of Nantes and spent 18 months as a postdoc at SRI International, Palo Alto, California. His main research interest concerns formal methods and their application to the analysis and verification of safety-critical systems. In the last few years, he has been working on extending the coinductive functions and proofs that can be accepted by the Coq proof assistant and on using Coq for proving the correctness of system-level code.

**Florin Stoican**

*Associated Researcher*

**Florin Stoican** is a professor in the Automatic Control department of the Politehnica University of Bucharest. Before that, he completed his PhD at Supelec (now CentraleSupelec, France) and was a postdoctoral fellow at NTNU (Norway). His research interests concern the application of set-theoretic methods into the fault tolerant control of dynamical systems through the prism of set-theoretic elements. Current work involves further research in set theory, constrained optimization problems and the coupling between motion planning, flat representations and spline approximations.

**Horia Velicu**

*Industry Advisor*

**Horia Velicu** is leading an Artificial Intelligence Hub within BRD Groupe Société Générale as part of the innovation stream of the bank. He is conducting several applied research projects in the banking domain, such as: transaction anomaly detection, predictive justice, recommender systems, etc. His main interests are reinforcement learning, algorithmic trading and machine learning for tabular data.

**Ulrich Kohlenbach**

*Honorary Member*

**Ulrich Kohlenbach** is a Professor of Mathematics at the Technische Universität Darmstadt (Germany). Previously, he was an Associate Professor of Computer Science at Aarhus University (Denmark). He received his PhD in Mathematics in 1990 and his Habilitation in 1995, both from the Goethe-Universität in Frankfurt. His main research area is mathematical logic and he is particularly interested in applying methods from proof theory to nonlinear analysis, ergodic theory, nonsmooth optimization and related areas (‘proof mining’). He was an Invited Speaker (Section: Logic and Foundations) at the 2018 International Congress of Mathematicians in Rio de Janeiro.

**Alin Ștefănescu**

*Executive Board*

**Alin Ștefănescu** is a Full Professor of Computer Science at the University of Bucharest. He enjoys collaborating with colleagues and students on various research projects at the frontier of the academic and industrial worlds. His main expertise is in software engineering with a focus on cybersecurity and software testing, using AI, model-based or formal methods. He was a researcher in several European universities (Technical University of Munich, University of Edinburgh, University of Stuttgart, University of Konstanz, University of Bucharest) and also has an extensive experience with industry, both as a member and as a team lead in R&D departments or collaborations with leading companies such as SAP, Bitdefender, and UiPath.

**Ciprian Păduraru**

*Research Collaborator*

**Ciprian Păduraru** is an Associate Professor at the University of Bucharest, as well as a machine learning researcher at Google and at the Simion Stoilow Institute of Mathematics of the Romanian Academy. His current research is focused on the safety of self-driving cars using computer vision techniques and automatic software testing. He uses fuzz testing and symbolic execution methods combined with deep learning and reinforcement learning. He has also worked in the game development industry for over 15 years, where he led teams on implementing AI in top video games.

**Marius Popescu**

*Research Collaborator*

**Marius Popescu** is an Associate Professor at the University of Bucharest, within the Department of Computer Science. He defended his PhD in 2004 with the thesis *Machine Learning Applied in Natural Language Processing*. His domains of interest are: artificial intelligence, machine learning, computational linguistics, information retrieval, authorship identification, computer vision. He is also a senior researcher in the tech startup SecurifAI and the director of the Center for Data Science of the University of Bucharest.

**Corina Păsăreanu**

*Research Collaborator*

**Corina Păsăreanu** is an ACM Distinguished Scientist, working at NASA Ames as Technical Professional Leader in Data Science. She is also affiliated with Carnegie Mellon University’s CyLab. Her research interests include model checking, symbolic execution, compositional verification, probabilistic software analysis, autonomy, and security. She is the recipient of several awards, including ETAPS Test-of-Time Award (2021), ASE Most Influential Paper Award (2018), ESEC/FSE Test of Time Award (2018), ISSTA Retrospective Impact Paper Award (2018), ACM Impact Paper Award (2010), and ICSE 2010 Most Influential Paper Award (2010). She has been serving as Program/General Chair for several conferences including: ICSE 2025, SEFM 2021, FM 2021, ICST 2020, ISSTA 2020, ESEC/FSE 2018, CAV 2015, ISSTA 2014, ASE 2011, and NFM 2009. She is currently an associate editor for the IEEE TSE journal.

**Radu Iosif**

*Research Collaborator*

**Radu Iosif** is a senior researcher at the French National Research Center (CNRS), Verimag laboratory in Grenoble. He graduated from the Politehnica University of Bucharest and obtained a PhD in Computer Science from Politecnico di Torino. His main research interest is system verification using logic and automata theory. Additional interests include formal languages, arithmetic, computability and complexity theory.

**Gheorghe Ștefănescu**

*Honorary Member*

**Gheorghe Ștefănescu** is an Honorary Professor of the University of Bucharest. He was a Computer Science professor at the University of Bucharest and director of its Computer Science Department and of its Computer Science Doctoral School. He received his PhD from the University of Bucharest under the supervision of Sergiu Rudeanu. Before joining the university faculty in 1995, he had spent 15 years as a researcher at the Institute of Mathematics of the Romanian Academy.

He has broad research interests spanning Computer Science, Mathematics, Biology, Cognitive Sciences, etc. In Computer Science his main research interests are in programming languages with an emphasis on formal methods as applied to distributed systems. In 1986 he has discovered an algebraic structure, named *biflow *(or *traced monoidal category*) and has developed *network algebras*, a uniform formalism covering algebraic models for both classical control structures (e.g., flowchart schemes) and distributed systems (e.g., dataflow networks). He wrote over 100 papers, has extensive visits abroad (including a 3 years Senior Fellow position at NUS/Singapore), has been offered several grants and awards (including the Grigore Moisil award of the Romanian Academy).

**Liviu Dinu**

*Research Collaborator*

**Liviu Dinu** is a Full Professor at the University of Bucharest, within the Department of Computer Science, Director of Human Language Technologies Research Center, and member of Computer Science and Interdisciplinary Doctoral Schools. His main research is in Computational Linguistics, Natural Language Processing (NLP), Information processing etc. Solomon Marcus was his PhD supervisor (obtained in 2003), and in 2014 he defended his habilitation thesis entitled *Similarity and Decision Problems in Computational Linguistics*. In 2007 he received the Grigore C. Moisil Prize awarded by the Romanian Academy (for 2005). He has initiated and managed a number of 13 national and international R&D projects and was involved in other 14 R&D projects. He has also initiated in 2020 a master program in Natural Language Processing at University of Bucharest.

**Mihai Prunescu**

*Research Collaborator*

**Mihai Prunescu** is an Associate Professor at the University of Bucharest and a researcher at the Simion Stoilow Institute of Mathematics of the Romanian Academy. He defended his PhD about Diophantine Definability at the University of Konstanz, Germany, in 1998. In 2011 he was awarded the Gheorghe Țițeica Prize of the Romanian Academy for a set of papers about recurrent 2-dimensional sequences over finite alphabets. His research interests are mainly in certain areas of mathematical logic, like decidability and definability in first-order theories, applications of model theory, unit-cost complexity over algebraic structures, recurrence over finite alphabets, set theory or the satisfiability of boolean formulas.

Recently, he became interested as well in concrete applications of mathematics like cryptography or security protocols.

**Cristian Rusu**

*Research Collaborator*

**Cristian Rusu** received the MSc and PhD degrees from the Politehnica University of Bucharest, Romania, in 2011 and 2012, respectively. He is currently an Associate Professor at the University of Bucharest, Romania, in the Department of Computer Science. His research interests include signal processing with applications to communications, sparse representations, dictionary learning, machine learning, and numerical linear algebra. In the context of signal processing, his research focuses on efficient algorithms for machine learning and the development of modern computing architectures.

**Pedro Pinto**

*Research Collaborator*

**Pedro Pinto** is a Research Assistant (‘Wissenschaftlicher Mitarbeiter’) in the Logic group of the Department of Mathematics at Technische Universität Darmstadt (Germany). He received his PhD in Mathematics in 2019 from the University of Lisbon (Portugal) for the study on the first applications of the bounded functional interpretation to mathematics. His current research area is the application of methods from proof theory to nonlinear analysis, convex optimization, fixed point theory and related areas (‘proof mining’).

**Cornelia Caragea**

*Research Collaborator*

**Cornelia Caragea** is a Professor of Computer Science at the University of Illinois Chicago (UIC), where she directs the Information Retrieval group. Prior to joining UIC, she was an Associate Professor at Kansas State University, where she received the Lloyd T. Smith Creativity in Engineering Endowed Chair and the Munson-Simu Keystone Research Scholar Award. She received her PhD in Computer Science from Iowa State University and her BSc in Computer Science and Mathematics from the University of Bucharest. Her research interests are in natural language processing, deep learning, information retrieval, and artificial intelligence with applications to text, image analysis, and social media. Cornelia Caragea’s work has been recognized with several NSF research awards, including the prestigious NSF CAREER award. She has published many research papers in top venues such as AAAI, IJCAI, WWW, EMNLP, ACL, and ACM Transactions on the Web and received several Best Paper Awards for her work with students in her group. She served as program committee member for many top conferences such as WWW, AAAI, ACL, NAACL, and EMNLP. Caragea also organized several workshops on scholarly big data co-located with IJCAI, AAAI, Big Data, and ACL.

**David Nowak**

*Research Collaborator*

**David Nowak** is a CNRS researcher at the University of Lille, France. His main research interest is formal verification applied to the safety and security of computer systems. In recent years he has been focusing of the use of the Coq proof assistant. After receiving his PhD in computer science from the University of Rennes in 1999, he was employed as a research officer at the University of Oxford until 2001. He was then appointed CNRS researcher: at École Normale Supérieure de Cachan (2001-2005); on secondment to the University of Tokyo (2005-2006); on secondment to the National Institute of Advanced Industrial Science and Technology (2006-2012); at the University of Tokyo (2012-2013); and at the University of Lille (since 2013).

**George Georgescu**

*Honorary Member*

**George Georgescu** is an Honorary Professor of the University of Bucharest. Before that, he was a Professor in the Computer Science Department between 1996 and 2011. Going further back, he defended his PhD in 1972 with a thesis on *θ*-valent Łukasiewicz algebras, written under the supervision of Grigore C. Moisil. He has published research in algebraic logic for non-classical logics, many-valued logics, sheaf representations in universal algebra, model theory for non-classical logics, quantale theory.

**Andrei Arusoaie**

*Research Collaborator*

**Andrei Arusoaie** is an Associate Professor at the Faculty of Computer Science, Alexandru Ioan Cuza University of Iași, Romania, where he is a senior member of the Formal Methods in Software Engineering research group. His research interests include programming language semantics, symbolic execution and formal verification of programs, formal verification and analysis of smart contracts. He has completed his PhD at the Alexandru Ioan Cuza University of Iași under the supervision of Dorel Lucanu. Afterwards, he was a postdoc at INRIA Lille Nord-Europe, where he was a member of the DREAMPAL team lead by Vlad Rusu.

**Alexandru Dragomir**

*Research Collaborator*

**Alexandru Dragomir** is currently a Teaching Assistant in the Faculty of Philosophy (University of Bucharest). He studied at the Faculty of Philosophy (BA, MA, PhD) and the Faculty of Mathematics and Computer Science (BSc) of the University of Bucharest. He completed his PhD with a thesis on Dynamic Epistemic Logic. His research interests include: epistemic logics and their applications in modelling security protocols, modal epistemology, the ethics of Artificial Intelligence, and the ethics of human enhancement technologies.

**Gabriel Istrate**

*Research Collaborator*

**Gabriel Istrate** is a Professor at the University of Bucharest. His research interests span various topics, mostly in Theoretical Computer Science. He has recently published papers on various topics in Algorithms, Computational Complexity, Algorithmic Game Theory and Multiagent Systems and Social Simulations. He received a PhD from University of Rochester (1999) and has previously held positions at Los Alamos National Laboratory and West University of Timișoara. He has recently published papers in venues such as ICALP, SAT, AAMAS, TARK.

**Toni Gibea**

*Research Collaborator*

**Toni Gibea** is currently an Assistant Professor at the Bucharest University of Economic Studies. He completed his PhD with a thesis on empirical and normative ethics. He is interested in applied ethics, experimental ethics and, more broadly, moral philosophy.

**Paulo Oliva**

*Research Collaborator*

Dr. **Paulo Oliva** is a computer scientist with a Ph.D. in Theoretical Computer Science. He is a world-leading expert in Mathematical Logic and Proof Theory, with over 50 internationally recognized research papers. He is currently a reader (associate professor) at Queen Mary University of London (QMUL), where he is the leader in the final year Web Programming module and the MSc Functional Programming module, and he is the department’s Director of Outreach.

**Thomas Powell**

*Research Collaborator*

**Thomas Powell** is a Lecturer (Assistant Professor) in the Mathematical Foundations group of the Department of Computer Science at the University of Bath (United Kingdom). He obtained his PhD in 2013 from Queen Mary University of London on the study of proof interpretations and their role in extracting computational content from proofs in mathematical analysis. He is primarily interested in applications of logic in both mathematics and computer science.

**Genaro López-Acedo**

*Research Collaborator*

**Genaro López-Acedo** is a Professor in the Department of Mathematical Analysis within the University of Seville. He defended his PhD thesis in 1987 with a thesis on metric fixed point theory, the results being basically contained in the book *Measures of Noncompactness In Metric Fixed Point Theory* written in 1997 together with J. M. Ayerbe and T. Domínguez, which was published by Birkhäuser as part of the prestigious book series Operator Theory. This book has become a basic reference for people working in metric fixed point theory. His research interests include convex optimization, monotone operator theory, proof mining, degree theory, fixed point theory and game theory.

**Bruno Dinis**

*Research Collaborator*

**Bruno Dinis** is an Auxiliary Professor at the University of Évora (Portugal). He received his PhD in Mathematics (Algebra and Logic) in 2013 from the University of Évora for developing an axiomatics for the External Numbers of Nonstandard Analysis. He has also been a Postdoc at the University of Lisbon, working mainly on nonstandard analysis, and functional interpretations and their applications.

**Cătălin Ciobanu**

*Industry Advisor*

**Cătălin Ciobanu** is the co-founder and CTO of Boostrs, a startup focusing on the science and importance of skills in the job market. Boostrs skill profile powers applications in Talent Management, Internal Mobility, Learning & Development, and Recruitment. He previously led Data & Analytics at CWT Solutions Group, a team of analysts, business intelligence specialists and data scientists. His strategy had three main priorities: advanced technical skills (R, Python), product innovation (web applications), and external communication (publications and conferences). Three of their studies have been published by the Harvard Business Review.

Prior to his industry experience he has worked as an experimental particle physicist. His PhD thesis research centered on using Artificial Intelligence to extract signal from large amounts of data.

**Denisa Diaconescu**

*Research Collaborator*

**Denisa Diaconescu** is an Associate Professor of Computer Science at the University of Bucharest (Romania). Her research interests are focused around applications of logic in computer science and formal verification of systems. Denisa completed her PhD in 2013 at the University of Bucharest under the supervision of George Georgescu. Afterwards, she was a postdoc researcher at the University of Bern (Switzerland) under the guidance of George Metcalfe.

Denisa is also a research consultant for Runtime Verification Inc., a formal-methods-based startup with the mission of building accessible trustworthy computing.

**Anton Freund**

*Research Collaborator*

**Anton Freund** is an Assistant Professor and Emmy Noether Group Leader (DFG) within the Logic Group at the Department of Mathematics at the Technical University of Darmstadt (Germany). Previously, he was a postdoc with Ulrich Kohlenbach at Darmstadt and did a PhD with Michael Rathjen at the University of Leeds (UK), which he completed in 2018. His research connects different approaches from logic (proof theory, reverse mathematics, set theory) with other areas of mathematics (combinatorics, dynamical systems) and computer science. He is particularly interested in relations between abstract non-computable objects and their concrete computational consequences.

**Florentina Hristea**

*Research Collaborator*

**Florentina Hristea** is currently a Full Professor in the Department of Computer Science of the University of Bucharest, Romania. She received a BSc degree in mathematics and computer science and a PhD degree in mathematics, both from the University of Bucharest, Romania, in 1984 and 1996, respectively. She received a habilitation in computer science, from the same university, in 2017. Her current research field is artificial intelligence, with specialization in: knowledge representation, natural language processing (NLP) and human language technologies (HLT), computational linguistics, as well as computational statistics and data analysis with applications in NLP. She has been Principal Investigator of several national and international interdisciplinary research-development projects and is Expert Evaluator of the European Commission in the fields of NLP and HLT. Professor Hristea is author or co-author of 9 books, 2 chapters in books and of various scientific papers out of which 32 are articles in peer reviewed scholarly journals. She is the author of an outlier detection algorithm which is named in her respect (Outlier Detection, Hristea Algorithm. Encyclopedia of Statistical Sciences, Second Edition, Vol. 9, N. Balakrishnan, Campbell B. Read, and Brani Vidakovic, Editors-in-Chief. Wiley, New York, p. 5885–5886, 2005) and is an elected member of ISI (International Statistical Institute). She is also a member of GWA (Global WordNet Association). Professor Hristea was a Fulbright Research Fellow at Princeton University, USA, an Invited Professor at the University of Toulouse, France and visiting scientist at: Heidelberg Institute for Theoretical Studies, Germany; University of Toulouse Paul Sabatier III, France; Institut de Recherche en Informatique de Toulouse, France; L’école Polytechnique “Polytech Montpellier”, France.

**Alexandru Corlan**

*Associated Researcher*

**Alexandru Corlan** is a research scientist at the University and Emergency Hospital of Bucharest. Both his MD and PhD degrees are from the Carol Davila University of Medicine and Pharmacy, Bucharest. His research interest were initially in digital electrocardiology, where he developed various indices and models for clinical prediction, partly during stages at the Universita degli studi din Milano and the Glasgow University. Later, he grew interested in the more general issues of the probabilistic predictive models based on population data, and the logic of their application in therapy policies, in collaboration with a group from the Stanford University. He is now preoccupied with the dynamics of research systems and the broader connection between the probabilistic logic of scientific prediction, the logic of policies and norms and their impact on health and other macroeconomic indicators.

**Fernando Ferreira**

*Research Collaborator*

**Fernando Ferreira** is a Professor of Mathematics at Universidade de Lisboa. He received his PhD at Pennsylvania State University in 1988 under the direction of Stephen Simpson. He was a Fulbright Scholar at Harvard University and Tinker Visiting Professor at Stanford University. He has written papers in weak systems of arithmetic and analysis, proof theory and logicism. He is now mainly interested in functional interpretations and the foundations of mathematics. He is a member of Academia das Ciências de Lisboa.

**Andrei Ilie**

*Research Collaborator*

**Andrei Ilie** is a PhD student at the University of Bucharest and an Engineering Manager for the Data Science Maps, Scooter, and Food teams at Bolt. He studied for his MCompSci and BA in Computer Science degrees at the University of Oxford, and he ranked top of his class in both. In his master’s degree, he focused on theoretical machine learning and formal logic, writing a thesis where he introduced a probabilistic extension of the CSL verification logic. At Bolt, Andrei has been building models for forecasting traffic patterns and travel ETAs, optimisation algorithms for optimal deployment of scooters, and models for forecasting food preparation times – all being used at a large-scale in Bolt’s active markets.

**Thomas Genet**

*Research Collaborator*

**Thomas Genet** is a full professor at the University of Rennes, France. He is interested in applying interactive and automatic deduction techniques to formal verification of programs. His long standing research subject concerns using term rewriting and tree automata techniques to prove safety properties of programs. He has also led several actions to popularize the usage of formal methods in security companies, such as the SPAN+AVISPA verification tool for cryptographic protocols. He has completed a PhD in computer science in 1998 at Nancy University under the supervision of Hélène Kirchner and Isabelle Gnaedig. In 2009 he got his Habilitation in Computer Science from Rennes University.

**Nicholas Pischke**

*Research Collaborator*

**Nicholas Pischke** is a PhD student in mathematics at TU Darmstadt supervised by Ulrich Kohlenbach. His main research interest is mathematical logic and proof theory, with a particular interest in finite type arithmetic and its applications in the proof mining program. He is also interested in modal, many-valued and intermediate logics and the resulting combinations thereof as well as their study through algebras and generalizations of sequent calculi.

**Mihai Cucuringu**

*Research Collaborator*

**Mihai Cucuringu** is an Associate Professor in the Department of Statistics, and an Affiliate Faculty in the Mathematical Institute at University of Oxford. He is also a Stipendiary Lecturer in Statistics at Merton College, University of Oxford, and a Turing Fellow at The Alan Turing Institute in London. Mihai finished his PhD in Applied and Computational Mathematics at Princeton University in 2012. Throughout 2013-2016 he was a CAM Assistant Adjunct Professor in the Department of Mathematics at UCLA.

**Dafina Trufaș**

*Research Student*

**Dafina Trufaş** is a second year Computer Science student at the University of Bucharest. She is passionate about programming and mathematics and has always found the idea of automatic theorem proving very interesting and wanted to learn more about it. In the fall of 2021, Dafina attended the Lean seminar, where she had the first contact with the functional programming paradigm and learned how to prove simple theorems and model some algebraic structures in Lean.

In the summer of 2022, Dafina completed an internship at Runtime Verification, where she had the opportunity to work for the first time in a proof-engineering team. There she learned the basics of theorem-proving in Coq, contributed some low-level code-tasks to the Correct-By-Construction Casper Project and was involved in improving the research paper and the documentation of this project.

**Viorica Sofronie-Stokkermans**

*Research Collaborator*

**Viorica Sofronie-Stokkermans** is a Professor of Computer Science at the University Koblenz, where she leads the group “Formal Methods and Theoretical Computer Science”. Previously, she was a senior researcher in the Automation of Logic Group at the Max Planck Institute for Informatics, Saarbrücken, Germany, leading the research area “Reasoning in Complex Theories”. She received her Habilitation in 2004 from the Saarland University, her PhD in 1997 from the Johannes Kepler University, Linz, Austria, and her diploma and specialization diploma in Computer Science and Mathematics from the University of Bucharest. Her main research interests are in classical and non-classical logic, automated reasoning and applications (in verification and knowledge representation and reasoning). She is especially interested in developing decision procedures for satisfiability checking in extensions and combinations of theories and in using these decision procedures for the deductive verification of reactive and hybrid systems.