### Former Associates

**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 the 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**

*Research Student*

**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**

*Associated Researcher*

**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 Student*

**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.

**Sergiu Nisioi**

*Associated Researcher*

**Sergiu Nisioi** is an Assistant Professor at the University of Bucharest. He works in areas adjacent to computational linguistics, covering topics such as psycholinguistics, computational learning theory, machine translation, and text simplification. In addition to his academic pursuits, he has also been active in the software industry for the past ten years, developing scalable machine learning pipelines.

**Cristian Kevorchian**

*Research Collaborator*

**Cristian Kevorchian** is an Associate Professor at the University of Bucharest’s Department of Computer Science. In 1995, he defended his PhD thesis on analogical reasoning applied to automated theorem proving, which he wrote under the supervision of Solomon Marcus. He has published work on topological approaches to multidimensional data, abduction ontology queries, blockchain applications in FINTECH (insurance industry), and cloud computing in data management.

**Nicolae Cleju**

*Associated Researcher*

**Nicolae Cleju** is an Associate Professor at the Gheorghe Asachi Technical University of Iași, Romania. He obtained the PhD degree in 2012, with a thesis on compressed sensing algorithms and applications. His research interests lie in the area of signal processing and machine learning, with a focus on sparse representations and associated optimization problems, and their applications for biomedical signals.

**Nicoleta Dumitru**

*Research Student*

**Nicoleta Dumitru** has finished the Advanced Studies in Mathematics master’s program at University of Bucharest. She is interested in concrete applications of mathematics like cryptography. Recently, she has become interested in proof mining and optimization.

**Claudia Chiriță**

*Research Collaborator*

**Claudia Chiriță** is a lecturer in Computer Science at the University of Bucharest. She completed her doctoral studies at Royal Holloway, University of London, where she then taught before joining University of Edinburgh as a lecturer. Her main research interests are formal specification, universal logic, and institution theory. Her current work focuses on hybrid-dynamic logics and non-standard logic programming.

**Ionuț Țuțu**

*Research Collaborator*

**Ionuț Țuțu** is a researcher at the Simion Stoilow Institute of Mathematics of the Romanian Academy. He finished his PhD in logic-independent logic programming at Royal Holloway, University of London, under the supervision of Professor José Fiadeiro. His research expertise lies in the area of algebraic specification and formal software development, often making use of category, model and institution theory.

**Julian Sutherland**

*Industry Advisor*

**Julian Sutherland** is the head of formal verification at Nethermind, a blockchain consultancy based in London. He completed his PhD with Prof. Philippa Gardner at Imperial college, focusing on the use of separation logic for compositional termination verification for fine-grained concurrency. He now leads a team that developed formal verification tools and formally verifies smart contracts, focusing particularly on the Ethereum and StarkNet ecosystem.

**Mădălina Erașcu**

*Research Collaborator*

**Mădălina Erașcu** is an Associate Professor in the Department of Computer Science of the West University of Timișoara, Romania. She holds a PhD in Technical Sciences from the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria. Her research is in developing algorithmic methods for building and maintaining reliable algorithms. To achieve this goal, she combines theoretical research in formal methods, satisfiability checking and symbolic computation motivated by practical applications in Cloud Computing, Big Data and Machine/Deep Learning.

She was involved in several projects funded by the European Commission and other research funding agencies (in Romania and Austria), as local team leader, member or PI. As an Innovation Researcher at Continental Automotive Romania SRL she was involved in the concept and development of a Sensor Error Model prototype as well as in Patent writing.

**Radu Ionescu**

*Research Collaborator*

**Radu Tudor Ionescu** is Professor at the University of Bucharest and Co-founder at SecurifAI. He completed his PhD at the University of Bucharest in 2013. He received the 2014 Award for Outstanding Doctoral Research in the field of Computer Science from the Romanian Ad Astra Association. His research interests include machine learning, computer vision, image processing, medical imaging, computational linguistics and text mining. He published over 110 articles at international peer-reviewed conferences and journals, and a research monograph with Springer. He received the “Caianiello Best Young Paper Award” at ICIAP 2013 for the paper entitled “Kernels for Visual Words Histograms”. Radu also received the “Young Researchers in Science and Engineering” Prize for young Romanian researchers, and the “Danubius Young Scientist Award 2018 for Romania” by the Austrian Federal Ministry of Education, Science and Research and by the Institute for the Danube Region and Central Europe. Together with other co-authors, he obtained good rankings at several international competitions: 4th place in the Facial Expression Recognition Challenge of WREPL 2013, 3rd place in the NLI Shared Task of BEA-8 2013, 2nd place in the ADI Shared Task of VarDial 2016, 1st place in the ADI Shared Task of VarDial 2017, 1st place in the NLI Shared Task of BEA-12 2017, 1st place in the ADI Shared Task of VarDial 2018.

**Bogdan Alexe**

*Research Collaborator*

**Bogdan Alexe** is an Associate Professor at the University of Bucharest, Romania. In 2013, he received his PhD degree at ETH Zurich. Since 2014 he joined the University of Bucharest, where he teaches lectures on computer programming, artificial intelligence and computer vision. His research interest include machine learning and pattern recognition in computer vision.

**Adrian Ispas**

*Industry Advisor*

**Adrian Ispas** is the CEO & Co-Founder of Vatis Tech, a company that provides speech recognition infrastructure for call centers and their mission is to provide an accurate and easy-to-use speech recognition API, for multiple fields, in multiple languages. Adrian has attended the University of Bucharest, where he received a BSc in Computer Science and a MSc in AI. Prior to founding Vatis Tech in March 2020, he worked as a software engineer.

**Florentin Ipate**

*Research Collaborator*

**Florentin Ipate** is a Full Professor in the Department of Computer Science, Faculty of Mathematics and Computer Science, University of Bucharest. His main research interests are in Formal Methods in Software Engineering, Membrane Computing and its applications, Model-based Testing and Search-based Software Testing. He holds a PhD in Computer Science from the University of Sheffield, an MSc in Software Systems Technology from the same university and an MEng in Computer Science and Automatic Control from the Politehnica University of Bucharest. He published over 120 papers and a research monograph with Springer. He has been visiting professor for various periods of time at the University of Sheffield; he is also honorary invited professor of the Xihua University, Chengdu. He is an editor of Springer’s Journal of Membrane Computing, in the steering committee of Conference on Membrane Computing and in the Bulletin committee of the International Membrane Computing Society and has been on the PC of leading conferences on Software Engineering and Membrane computing. He has been (local) PI in several RTD projects, including 2 EU collaborative projects.

**Gilda Ferreira**

*Research Collaborator*

**Gilda Ferreira** is an Assistant Professor at Universidade Aberta, Portugal, where she serves as the coordinator of the Mathematics Section. She is a member of the Center of Mathematics, Fundamental Applications and Operations Research, and also collaborates with the Lasige Computer Science and Engineering Research Centre. In 2006, she obtained her PhD from the Faculty of Sciences at the University of Lisbon under the supervision of Fernando Ferreira. Following her doctoral studies, she did a three-year postdoc at Queen Mary University of London with Paulo Oliva. Her research interests lie in the field of Mathematical Logic, with a particular focus on proof theory. Her work encompasses various topics, including polymorphism, realizability and functional interpretations, bounded arithmetic, and weak analysis.

**Ionel Popescu**

*Research Collaborator*

**Ionel Popescu** got his bachelor degree from the Faculty of Mathematics of the University of Bucharest and his Ph.D from MIT. After a postdoc at Northwestern University, he had an assistant/associate professor position at Georgia Tech but now he is a full professor at the University of Bucharest in the Faculty of Mathematics and Computer Science and he also holds a researcher position at the Institute of Mathematics “Simion Stoilow” of the Romanian Academy. He is, by training, a mathematician with a focus on probability and machine learning at the moment, however, he consider himself an analyst with a general interest in multidisciplinary areas which can be related to biology, numerical analysis, computer science, data science, statistics and finance.

**Eugenio Omodeo**

*Research Collaborator*

**Eugenio G. Omodeo** is a Senior Scholar at the University of Trieste, within the Department of Mathematics and Earth Sciences. He received a degree in Mathematics in 1975 at the University of Padova, then Master of Science and PhD degrees in Computer Science at the New York University in 1979 and 1984, where his supervisor was Martin Davis. From 1981 to 1989, he was employed by companies belonging to ENI, the National Hydrocarbon Company of Italy, where he became coordinator of R&D activities of Enidata in the area of Advanced Information Processing. His team took part in several Esprit projects funded by the European Commission. He then became a professor and worked for several Italian Universities (Udine, “La Sapienza” of Rome, Salerno, L’Aquila, Trieste) before entering retirement in 2020. His scientific publications include 4 monographs, over 60 articles and 40 contributions to conference proceedings. Main fields of interest: Automated reasoning, Computational logic, Proof verification, Computable set theory.

**Andrea Sgarro**

*Research Collaborator*

**Andrea Sgarro** is a *studioso senior* (senior scientist) at the University of Trieste (I). His current scientific interests are fuzzy arithmetic and computational linguistics, while he has previously worked in information theory (Shannon theory), coding theory, cryptography, soft computing and fuzzy logic, incomplete (partial) knowledge management. He is quite active in scientific communication: his two books *Codici segreti*, Mondadori (translated into several European languages) and *Crittografia*, Muzzio, have introduced for the first time the new cryptography to an Italian-speaking audience. In his free time he studies, reads and speaks languages (he lectured in five different languages) and plays the baroque transverse flute. His main mentors have been Solomon Marcus, Bucharest, Giuseppe O. Longo, Trieste, and Janos Körner, Budapest and Rome, Shannon Prize. He is with Gruppo Nazionale di Calcolo Scientifico of the Istituto Nazionale di Alta Matematica and director of the Scientific Section of the Circolo della Cultura e delle Arti di Trieste. He co-operates closely with Bucharest University (Ro), prof. Liviu P. Dinu, and York University (UK), prof. G. Longobardi.

**Traian Rebedea**

*Associated Researcher*

**Traian Rebedea** is an Associate Professor at the Politehnica University of Bucharest and a Senior Researcher at NVIDIA. After completing his PhD at the Politehnica University of Bucharest, with a thesis focused on discourse analysis for multiparty dialogues in Computer Supported Collaborative Learning (CSCL), Traian continued his work as a professor and researcher, focusing on applied research projects in opinion mining, social network analysis, information retrieval and conversational agents. In addition to his academic research work at the Faculty of Automatics and Computer Science, UPB, he was Chief Data Scientist and co-founder at RoboSelf, where he developed Colang – a language for modelling conversational flows, and currently continues his work at NVIDIA as Principal Scientist in the Dialogue Systems team.

**Bogdan Gheorghe**

*Associated Researcher*

**Bogdan Gheorghe** is a PhD student at the Polytechnic University of Bucharest. He is also a Teaching Assistant at the same university, where he teaches: computer programming, data structures and algorithms, and object-oriented programming. His main research fields of interest are: UAV control, multi-agent systems, stability analysis, model predictive control.

**Theodor-Gabriel Nicu**

*Associated Researcher*

**Theodor-Gabriel Nicu** is a PhD Student and Teaching Assistant in the Automatic Control and Systems Engineering Department of the Politehnica University of Bucharest, Romania. He received BSc and MSc degrees in the Systems Engineering domain from the Politehnica University of Bucharest, Romania, in 2020 and 2022, respectively. His current research interests focus on Mixed-Integer representations, the Artificial Potential Field approach for obstacle collision avoidance algorithms and also B-spline representations.

**Vladimir Antofi**

*Research Student*

**Vladimir Antofi** is a second year Bachelor’s student in Mathematics at the University of Bucharest. His passions include mathematics, logic and linguistics. He is interested in learning about how proof systems work and the axiomatization of mathematics as a whole both in the context of set theory and of proof assistants such as Coq and Lean.

**Mihaela Florea**

*Associated Researcher*

**Mihaela Florea** received her Ph.D. in Chemistry in 2003 from the University of Louvain la Neuve (Belgium). In February 2004, she joined the group of catalysis from the Faculty of Chemistry, University of Bucharest where she began her research on heterogenous catalysis, especially on catalytic selective oxidation. From 2017, she starts the collaboration with National Institute of Materials Physics, and from 2021 she is the head of the of Catalytic Materials and Catalysis Group. Central to Mihaela’s research interests is the design of materials for modern catalysis and energy applications. This includes synthesis and properties investigation of new mixed metal oxides, metal carbides, nitrides and oxynitrides and design of new approaches for the synthesis of organic-inorganic halide perovskite-type materials with ferroelectric properties for photovoltaic applications. Her research activities also focus on development of electrocatalysts for OER, HOR and ORR reactions and use 2D materials like graphenes and MXenes for catalytic applications, such as water splitting, chemoselective hydrogenation and selective oxidation reactions.

**Florentina Neațu**

*Associated Researcher*

**Florentina Neațu**, scientific researcher 1st degree at the National Research and Development Institute for Materials Physics, earned her Ph.D. in Chemistry from the University of Bucharest’s Faculty of Chemistry in 2009. Research interests in the area of heterogeneous catalysis, and more specifically green and sustainable chemistry, include the discovery of acidic heterogeneous catalysts for PET depolymerization and the development of alternative methods for the synthesis of important monomers in the polymer industry that make use of renewable resources. She is an expert in a wide range of fields, including the development of novel catalytic methods for performing hydrogenation and selective oxidation reactions, and the fabrication of solid catalysts using a number of different approaches.

**Ștefan Neațu**

*Associated Researcher*

**Ștefan Neațu**, who is currently working as a scientific researcher 2nd degree at the National Institute of Materials Physics, received his Ph.D. in Chemistry from the University of Bucharest’s Faculty of Chemistry in 2010. Ștefan Neațu’s primary research areas following the completion of his doctoral studies include the preparation and characterization of active photocatalysts, the design and optimization of photocatalytic reactions, heterogeneous catalysis and associated chemical transformations, as well as energy and fuels, among other topics. Throughout his scientific tenure, he has acquired considerable expertise in the utilization of scientific instrumentation and the execution of experimental protocols. Moreover, his research experience has provided him with the proficiency to utilize these techniques in clarifying the physicochemical phenomena of different catalytic reactions.

**Alexandru Oltean**

*Research Student*

**Alexandru Oltean** is a master’s student in the Security and Applied Logic program at the University of Bucharest. Previously, he studied Computer Science (BSc) and Philosophy (BA) at the same university. He is interested in logic and its applications to computer science. He recently started exploring the field of computer verification, gaining an initial introduction by using the Lean proof assistant to formalize hybrid modal logic.

**Mihai Mașala**

*Associated Researcher*

**Mihai Mașala** is a Ph.D. student at the Romanian Academy working on bringing together computer vision and natural language processing. Before starting his Ph.D., he worked on Natural Language Processing with a strong focus on question answering techniques and chat conversations analysis. His current research involves bridging the gap between vision and language by using graphs of events in space and time.

**Miruna-Andreea Zăvelcă**

*Associated Researcher*

**Miruna-Andreea Zăvelcă** is a teaching assistant at the Faculty of Mathematics and Computer Science of the University of Bucharest and a PhD student in Artificial Intelligence supervised by Gheorghe Ștefănescu. Her main area of interest is Natural Language Processing with a strong focus on argumentation and proof.

**Alexandru Dima**

*Associated Researcher*

**Alexandru Dima** is a PhD student at the Faculty of Automatic Control and Computer Science, UNST Politehnica Bucharest. He holds a Bachelor’s degree in Computer Science and a Master’s degree in Artificial Intelligence (AI), with experience as a teaching assistant for courses like object-oriented programming and algorithm design. He has more than two years of practical experience in AI, machine learning (ML) and deep learning (DL), through national research projects. While his research experience is mostly focused on natural language processing (NLP), he is also passionate about visual and auditory data modalities.

**Isabela Drămnesc**

*Research Collaborator*

**Isabela Drămnesc** is Associate Professor in the Department of Computer Science of Faculty of Mathematics and Computer Science from West University of Timișoara. Her research interests include: logic; automated reasoning; mathematical theory exploration; algorithm synthesis, verification and transformation. She received her PhD in Computer Science in 2013 from the West University of Timișoara under the supervision of Tudor Jebelean from Johannes Kepler University, Linz, Austria. Afterwards, she was a postdoc at West University of Timișoara and at INRIA, Sophia-Antipolis, France. She has experience in European projects both as a member, and also as a manager of the Erasmus+ projects strategic and cooperation partnerships for higher education “ARC: Automated Reasoning in the Class”, “AiRobo: Artificial Intelligence based Robotics”. She received in 2020 the “Mihail Ghermănescu” award for Mathematics and Computer Science from the West University of Timișoara at the sixth edition of Gala Premiilor UVT.