Wenxi Wang is an Assistant Professor in the Department of Computer Science at the University of Virginia. His research focuses on enhancing software reliability and security through the integration of formal methods and machine learning, particularly in areas like SAT solving, graph neural networks, and cloud access control. He holds a Ph.D. from the University of Texas at Austin and an MPhil from the University of Melbourne. Education Ph.D., University of Texas at Austin (2024) MPhil (Research Master's), University of Melbourne Research Interests Wenxi Wang’s work bridges software engineering, security, formal methods, and machine learning. Key areas include: - Software reliability (especially for AI systems) - Verification and validation techniques - SAT solving and automated reasoning (e.g., SMT solving) - Graph neural networks and reinforcement learning applications Awards MIT EECS Rising Stars (2022) George J. Heuer, Jr. Ph.D. Fellowship (2023–2024) Service & Leadership He serves on program committees for top venues like ICSE, CAV, and ASE, and chairs sessions on verification and testing at ECOOP and ASE. His group, the Hiprel Group, actively develops tools like NeuroBack and DataBack to advance SAT solving and software reliability. Labs/Groups Leads the Hiprel Group , focused on integrating machine learning with formal methods for secure software systems.
Ronald de Haan is an Assistant Professor at the Institute for Logic, Language & Computation (ILLC) , University of Amsterdam, with primary affiliation in Theoretical Computer Science (TCS) and secondary affiliation in Mathematical & Computational Logic (MCL) . Since December 2019, he has held this position, following a postdoctoral role at the same institution from 2017 to 2019. He completed his PhD at the Algorithms and Complexity Group at Technische Universität Wien in 2016. Education: PhD in Computer Science, Technische Universität Wien (2016) MSc in Computational Logic, European Master's Program in Computational Logic (2010–2012) BSc in Cognitive Artificial Intelligence & BA in Linguistics, Utrecht University (2007–2010) Research Interests: His work lies at the intersection of theoretical computer science and artificial intelligence , with a strong emphasis on parameterized complexity theory . He explores the computational complexity of problems in AI, knowledge representation & reasoning, and computational logic. Specific areas include the Polynomial Hierarchy, subexponential-time complexity, the Exponential Time Hypothesis, and parameterized compilability. Scientific Awards: E.W. Beth Dissertation Prize 2017 for his PhD thesis "Parameterized Complexity in the Polynomial Hierarchy" Shortlisted for the Heinz Zemanek Prize 2018 Nominated for the GI-Dissertationspreis 2016 by the German Informatics Society Teaching & Supervision: He has taught a wide range of courses at the University of Amsterdam, including Computational Complexity , Knowledge Representation and Reasoning , and Recursion Theory for MSc Logic and MSc AI programs. He also supervises student research projects and theses, offering topics in ASP, complexity theory, and logic programming. Academic Service: He has served on the program committees of top-tier AI and logic conferences such as AAAI, IJCAI, KR, ECAI, and AAMAS, and co-organized events like PhDs in Logic VII.
Carmine Dodaro is an active researcher in Answer Set Programming (ASP) at the University of Calabria's Department of Mathematics and Computer Science. With over 130 publications from 2011-2025, his work bridges theoretical advances in logic programming with practical healthcare applications. His primary research interests include: Answer Set Programming theory and implementation Compiler techniques for ASP solvers Healthcare scheduling optimization (operating rooms, nurse staffing, chemotherapy) Integration of ASP with other AI paradigms Real-world constraint satisfaction problems Dodaro's recent work demonstrates exceptional focus on healthcare applications of ASP, with multiple 2023-2024 publications addressing nurse scheduling, operating room management, rehabilitation planning, and nuclear medicine scheduling. His approach typically involves developing specialized ASP encodings that handle complex real-world constraints while maintaining computational efficiency. He maintains a highly productive collaboration network, particularly with Marco Maratea (52 co-authored papers), Mario Alviano (40), and Giuseppe Galatà (23), forming one of Italy's leading ASP research groups. His publications appear consistently in top venues including Theory and Practice of Logic Programming, IJCAI, AAAI, and specialized logic programming conferences. Dodaro has contributed significantly to both theoretical foundations (unsatisfiable core analysis, paracoherent reasoning) and practical implementations (WASP solver extensions, CNL2ASP translation tools). His 2024-2025 publications indicate ongoing research momentum with no signs of reduced activity.
Marek Adamek is a researcher affiliated with the Institute of Computer Science at the Faculty of Electronics and Information Technology, Warsaw University of Technology. His institutional email is M.Adamek@ii.pw.edu.pl, and he maintains an external academic profile in the university repository. His research focuses on formal methods in software engineering, particularly temporal logic applications for code analysis. Key interests include: Line-of-code metrics and verification Kripke structure modeling Parallel programming constraints SAT solving for temporal logic (LTL) Software validation through formal methods His bibliometric profile shows 3 publications with a Scopus h-index of 1, total SNIP of 0.846, and CiteScore of 1.33. The Polish Ministry of Science awards him a cumulative score of 50 based on his research output. Awards and metrics: Scopus h-index: 1 (including autocitations) Total SNIP: 0.846 Total CiteScore: 1.33 Ministry Score: 50 He completed his PhD in 2019 with research centered on temporal logic applications in software engineering. His work bridges theoretical computer science and practical code analysis, particularly in parallel programming environments.
Vasco Manquinho is an Associate Professor affiliated with the University of Lisbon. He is actively involved in the Software Algorithms and Tools for Constraint Solving (SAT Group) , focusing on computational logic and constraint-solving algorithms. His teaching responsibilities include Introduction to Algorithms and Data Structures , Algorithms for Computational Logic , and Automatic Reasoning and Computational Logic . Emails: vasco.manquinho@tecnico.ulisboa.pt vasco.manquinho@inesc-id.pt
Dr. Fang Yu is an Associate Professor at the Department of Management Information Systems, National Chengchi University, specializing in software security, formal verification, and string analysis. They hold a Ph.D. in Computer Science from the University of California, Santa Barbara. Research Expertise: Dr. Yu focuses on cybersecurity, formal methods for software verification, and machine learning applications in data clustering and adversarial example detection. Their work bridges theoretical computer science with practical security solutions. Publication Trends: Recent articles address biomedical data clustering ( scGHSOM ), explainable AI ( XFlag ), and adversarial defense mechanisms. Topics span bioinformatics, security verification, and fairness testing in neural networks. Awards: 資深優良教師(10年) (2020, National Chengchi University) 國科會研究獎勵 (2019, National Science Council, Taiwan) Projects: Principal Investigator for 15+ grants from Taiwan's National Science and Technology Council and Ministry of Education, focusing on AI security, IoT verification, and financial technology.
Victor Lagerkvist is an Associate Professor at the Department of Computer Science (IDA) , Linköping University, Sweden. He is affiliated with the Theoretical Computer Science Laboratory (TCSLAB) and the Artificial Intelligence and Integrated Computing Systems (AIICS) division. His research focuses on the algebraic method for analyzing computational complexity , particularly in constraint satisfaction problems (CSPs), SAT, and graph homomorphism problems. PhD in Computer Science (2016, Linköping University) Habilitation (2020, Linköping University) His recent work investigates fine-grained complexity , twin-width , and universal algebra to improve algorithms for NP-hard problems. Publications span topics like propositional abduction, Allen's interval algebra, and semiring-based dynamic programming. His scientific awards include the Swedish Research Council Starting Grant (2020) and the 2017 Young Researcher Prize from the Ruth and Nils-Erik Stenbäck Foundation. He supervises PhD students such as Leif Eriksson and serves as a secondary supervisor for others at Linköping University and Université de Lorraine.
Aleksandar Zeljić is a Researcher at Stanford University's Center for Automated Reasoning and Center for AI Safety . He holds a PhD from Uppsala University's Department of Information Technology, supervised by Philipp Ruemmer, Christoph M. Wintersteiger, and Wang Yi. Research Focus: Automated reasoning (SAT/SMT solvers), formal verification of deep neural networks, and machine arithmetic analysis. Projects: Marabou (neural network verification), UppSAT (SMT approximation framework), mcBV (bit-vector SMT solver), and SmallFloats (Z3-based floating-point approximation). His recent publications focus on bit-vector interpolation, neural network optimization, and parallel verification techniques. Articles reveal expertise in formal methods , symbolic computation , and AI safety . Notable recognition includes the IJCAR Best Paper Award (2014) . Contributions to theoretical computer science include: Developing approximation frameworks for SMT solvers Advancing bit-vector and floating-point arithmetic verification Creating parallelization strategies for neural network analysis He has served as PC member for conferences like VSSTE, PAAR, and FOMLAS, and reviewed for journals including TCS and JAR.
Carla Gomes is a Professor at Cornell University and a leading figure in Artificial Intelligence (AI), renowned for pioneering the field of Computational Sustainability. Her work bridges core AI advancements with multidisciplinary research, addressing critical sustainability challenges while driving innovation in computer science. Key Contributions: Established Computational Sustainability as a transformative subfield integrating computational methods with ecological and socio-economic problem-solving. Developed XOR-streamlining for model counting, enabling breakthroughs in probabilistic inference and combinatorial solvers. Advanced AI applications in materials discovery, including Deep Reasoning Networks for solving crystal-structures phase-mapping problems to identify solar fuel materials. Awards: ACM AAAI Allen Newell Award (2021) for foundational AI and Computational Sustainability contributions. Recognized as an ACM Fellow (2017) for transformative work in AI and technology advancement. Gomes’ research spans combinatorial optimization, heavy-tailed runtime distributions, and algorithm portfolios, with practical impacts on SAT, MIP, and SMT solvers. Her NSF Expeditions awards underscore her leadership in fostering interdisciplinary collaboration for global sustainability solutions.
Ashutosh Trivedi is an Associate Professor of Computer Science at the University of Colorado Boulder, currently on leave from his position as Assistant Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology Bombay. He is affiliated with multiple research initiatives including the Centre for Formal Design and Verification of Software (CFDVS) at IIT Bombay, Free and Open Source Software for Education (FOSSEE), and the Indo-French project on Algorithmic Verification of Real-Time Systems (AVeRTS). At CU Boulder, he leads the Programming Languages and Verification (CUPLV) research group focusing on trustworthy AI systems. Trivedi's research centers on bridging formal methods with artificial intelligence to create more trustworthy systems. His work spans formal verification of cyber-physical systems, reinforcement learning with formal guarantees, and developing techniques for ensuring software fairness and accountability. He specializes in using formal languages, automata, and logic to transform vague natural-language instructions into precise specifications for AI systems. His recent projects include developing reinforcement learning algorithms for cardiac pacemaker design based on formal safety requirements, using SAT solvers to ground large language model outputs in logical reasoning, and encoding state representations in reinforcement learning using formal languages. His publication trends reveal a strong focus on neurosymbolic approaches that combine neural networks with symbolic reasoning, particularly for safety-critical applications. Recent work demonstrates increasing integration of formal methods with reinforcement learning, with applications spanning medical devices, tax preparation software, and puzzle-solving AI. His research shows a clear trajectory toward making AI systems more explainable, accountable, and verifiable through principled mathematical frameworks. Distinguished Paper Award at CAV for Regular Reinforcement Learning (2024) NeuS 2025 Disruptive Idea Award for Stochastic Neural Simulation Relations for Transferring Control under Uncertainty ACM Senior Member recognition (2024) Royal Society Wolfson Visiting Fellowship (2024) Trivedi has successfully advised multiple PhD students to completion, including Shadi Tasdighi Kalat (2025), Mateo Perez (2025), John Komp (2024), Vishnu Murali (2024), and Taylor Dohmen (2024). His teaching portfolio includes foundational courses in automata theory, digital logic design, and cyber-physical systems at both IIT Bombay and CU Boulder. He has served on program committees for major conferences including FSTTCS, HSCC, and FORMATS, and organized workshops such as ICLA 2015 and ALC 2015. As leader of the CUPLV research group, Trivedi directs projects focused on formal verification of AI systems, reinforcement learning with safety guarantees, and software fairness. His group collaborates with medical researchers on cardiac device verification and with legal scholars on tax software accountability, reflecting his commitment to applying formal methods to real-world problems with significant societal impact.
Lakhdar Sais is a Professor of Computer Science at the Centre de Recherche en Informatique de Lens (CRIL), CNRS UMR 8188, at Université d'Artois, Faculty of Jean Perrin Sciences in Lens, France. His research focuses on search and representation problems in Artificial Intelligence, including propositional satisfiability, quantified boolean formulas, constraint programming, knowledge representation and reasoning, data mining, and AI applications in Social and Human Sciences. He has supervised numerous PhD students throughout his career, with recent students including David ING (2021-present) working on migration data knowledge extraction, and previously Ikram NEKKACHE (2021), Sofiane TOUATI (2021), and Kahina BOUCHAMA (2020). His research has been recognized with multiple awards including best paper awards at SAT'11 and ICTAI'2009, and first place in the International SAT 2009 competition. His current research projects include the ANR project HYCI (2023-2026) on Hyper-places, Crises, Migrations and Inequalities, Project ERA (2022-2025) on producing new knowledge in juvenile justice and mental health, and ANR project POSTCRYPTUM (2021-2023) on algebraic cryptanalysis for post-quantum cryptography. He has also edited the Handbook of Parallel Constraint Reasoning (Springer, 2018). Scientific Awards: Best paper award at SAT'11 for 'On freezing and reactivating learnt clauses' Best paper award at ICTAI'2009 for 'Learning for Subsumption' ManySAT - First rank at International SAT 2009 competition (Parallel Track) LySAT - Two bronze medals at International SAT 2009 competition (Sequential Track) ManySAT - First rank at SAT Race 2008 competition Professor Sais has taught numerous courses including Artificial Intelligence, Constraint Programming, Knowledge Representation and Reasoning, Expert Systems, Complexity Theory, Advanced Data Structures, Algorithmics, and Functional Programming. He has served as leader of the inference and decision process research group at CRIL (2002-2013) and as Delegate Director of the CRIL laboratory (2013-2018).
Eric Reiner serves as an Adjunct Professor of Finance and Faculty Director of the Master of Financial Engineering program at UCLA Anderson School of Management. His unique academic profile bridges finance and formal methods, combining financial engineering expertise with advanced computational verification techniques. Dr. Reiner's research spans two distinct domains: traditional finance and formal methods in computer science. His work in formal methods focuses on satisfiability modulo theories (SMT), bit-precise reasoning, and model checking, with publications appearing in leading formal methods venues. This unusual interdisciplinary approach suggests innovative applications of verification techniques to financial systems, potentially addressing challenges in algorithmic trading verification, risk model validation, and financial protocol security. Analysis of his recent publications (2022-2024) reveals a strong focus on improving SMT solver capabilities, particularly for bit-vector reasoning and user extensibility. His work shows progression from theoretical foundations toward practical industrial applications, with increasing attention to proof generation, solver performance optimization, and machine learning techniques for algorithm selection. The consistent publication record in formal methods venues indicates deep technical expertise that complements his finance role. As Faculty Director of the Master of Financial Engineering program, Dr. Reiner oversees curriculum development that likely integrates both traditional finance knowledge and cutting-edge computational verification methods. This distinctive combination prepares students to develop and validate complex financial algorithms with mathematical rigor, addressing growing industry needs for verified financial technologies.
Elvira Albert is a Professor in the Department of Computer Systems and Programming at the School of Computer Science, Complutense University of Madrid, Spain. She leads the COSTA research group, which specializes in formal methods for program optimization and verification, with a strong focus on blockchain technologies and smart contracts. She holds a Ph.D. in Computer Science. Her research encompasses program verification, static analysis, and compiler construction, particularly applied to blockchain ecosystems. The COSTA group has developed influential tools including circom (for arithmetic circuit compilation), CIVER (for circuit verification), EthIR (EVM decompiler), and superoptimizers such as GASOL and SuperStack. Recent publications (2019-2024) demonstrate her expertise in smart contract safety (e.g., SAFEVM), concurrency testing, and bytecode superoptimization using constraint solvers. Her work consistently bridges theoretical formal methods with practical tool development for the blockchain industry. Albert has secured substantial funding from the Ethereum Foundation for multiple projects (GASOL, GREEN, SOPA, FORVES series, ZK-ARCKIT, GREY). She serves as an area editor for Theory and Practice of Logic Programming (TPLP) since 2019. The COSTA group, under her leadership, maintains an active research agenda in blockchain verification, zero-knowledge proofs, and formally verified compilers. Current projects include ZK-ARCKIT for arithmetic circuit analysis and FORYU for formal semantics of Yul.
José Fragoso Santos is an Assistant Professor in the Department of Computer Science and Engineering at Instituto Superior Técnico, University of Lisbon, and a member of INESC-ID where he conducts research as part of the SAT group. His research focuses on embedding formal methods into software development processes, with particular emphasis on JavaScript program analysis and verification. His educational background includes: PhD in Computer Science from University of Nice Sophia Antipolis (2014) Master's degree in Information Systems and Computer Engineering from Instituto Superior Técnico, Universidade de Lisboa (2008) Dr. Santos' research centers on JavaScript verification, symbolic execution, and secure information flow. He led the development of JaVerT, the first separation-logic-based tool for JavaScript analysis and testing, which has gained significant interest from both industry and academia. His work bridges theoretical formal methods with practical applications, particularly in web security and program analysis. He has made substantial contributions to understanding JavaScript semantics, symbolic execution techniques, and secure information flow in web applications, with publications in premier venues like PLDI, POPL, and ECOOP. His recent publications demonstrate a strong focus on symbolic execution for JavaScript and related languages, with applications in web security and program verification. The research shows progression from foundational work on information flow security to advanced techniques like compositional symbolic execution and multi-language analysis platforms. His work on JaVerT and Gillian has established significant research directions in program analysis for dynamic languages. His notable scientific achievements include: Facebook research award for the JaVerT project Dr. Santos has supervised numerous graduate students on projects related to JavaScript verification, symbolic execution, web security, and formal methods. His research has practical applications, as evidenced by the collaboration with Amazon R&D engineers to verify critical components of the AWS Encryption SDK using JaVerT. He has served on program committees for major conferences including PLDI, OOPSLA, and IJCAI, demonstrating his standing in the programming languages community. As a member of the SAT group at INESC-ID, Dr. Santos collaborates with researchers working on formal methods, program verification, and software security. His current projects include extending JavaScript symbolic execution to Web Workers, developing formal semantics for JavaScript regular expressions, and creating first-order solvers for program analysis. He continues to push the boundaries of what's possible in JavaScript program analysis and verification.
Magnus O. Myreen is a Professor in the Department of Computer Science and Engineering at Chalmers University of Technology, Sweden. He has been with Chalmers since 2014, becoming a tenured Associate Professor in 2015 and being promoted to full Professor in June 2023. Myreen has an extensive record of service to the programming languages and formal methods communities, including serving on program committees for major conferences like PLDI, POPL, ICFP, and CPP, and chairing the steering committee for the ITP conference series since November 2023. Myreen received his academic training at prestigious institutions: B.A. in Computer Science at the University of Oxford, tutored by Dr. Jeff Sanders Ph.D. on program verification in 2009 at the University of Cambridge, supervised by Prof. Mike Gordon Myreen's research focuses on program verification, interactive theorem proving, and compiler verification. He is best known for his work on the CakeML project, which is an ML-style language with a formal semantics and a growing ecosystem of proofs and tools that support construction of verified applications. As he states on his website, "My most recent work has focused on CakeML, which is an ML-style language with a formal semantics and a growing ecosystem of proofs and tools that support construction of verified applications. As far as I know, the CakeML compiler is the first verified compiler to have been bootstrapped." His research spans several key areas: Decompilation into logic — verification of machine code Proof-producing synthesis from logic Verified Lisp and ML runtimes Connecting things up: verified stacks Myreen's publication record shows a strong focus on verified compilation and theorem proving, particularly through the CakeML ecosystem. His work consistently bridges the gap between theoretical foundations and practical implementation, with numerous papers on verified compilers, program verification, and theorem proving. A significant trend in his recent work (2021-2024) has been extending CakeML's capabilities to handle more complex language features, improve performance, and verify increasingly sophisticated compilation techniques including bootstrapping and dynamic computation. Myreen has received several prestigious awards and recognitions: Winner of the BCS Distinguished Dissertation Competition 2010 for his PhD work Royal Society Research Fellow (UK) since 2012 ACM SIGPLAN Most Influential POPL Paper Award for the 2014 CakeML paper Amazon Research Award for his proposal "Compiling Dafny to CakeML" Myreen has advised several PhD students to completion, including Alejandro Gomez (Sep 2017 – Jun 2023), Oskar Abrahamsson (Aug 2017 – Dec 2022), and Andreas Loow (Sept 2016 – Sep 2021). He also collaborated with postdocs including Hira Syeda, Thomas Sewell, and Johannes Aman Pohjola. His research has been supported by various funding sources, though specific grants aren't detailed in the provided text. Notably, he received an Amazon Research Award for his work on compiling Dafny to CakeML, and his CakeML project has clearly attracted significant attention in the programming languages and formal methods communities. Myreen leads research on the CakeML project, which has grown into a substantial ecosystem for verified compilation. The project involves a team of researchers working on various aspects including compiler verification, program synthesis, and theorem proving. Myreen also collaborates with researchers at other institutions, as evidenced by his visits to EPFL (meeting Viktor Kuncak, Martin Odersky, and James Larus) and NUS (visiting Ilya Sergey's group). In October 2023, he began a ten-month sabbatical at Cambridge UK, where he worked part-time for Arm Ltd., indicating ongoing industrial collaboration.
