Dr. Martin Bromberger is a Senior Researcher at the Max Planck Institute for Informatics, specializing in Automated Reasoning , Linear Arithmetic , and Theorem Proving . He is affiliated with the Automation of Logic research group (RG1), focusing on combinations of theories and arithmetic reasoning. His recent work includes publications at top venues like TACAS, FroCoS, and VMCAI. He has developed critical SMT solvers such as SPASS-IQ and SPASS-SATT , advancing constraint-solving techniques in linear arithmetic. His research spans Arithmetic Decision Procedures Datalog Applications Bernays-Schoenfinkel Fragment Cube-Based Arithmetic Optimization He received awards at SMT-COMP 2018, SMT-COMP 2019, and the Best Student Paper Award at CADE-27 for his contributions to SMT solving.
Thomas Sturm is a CNRS Research Director at LORIA in Nancy, France, and affiliated with the Max Planck Institute for Informatics and Saarland University in Saarbrücken, Germany. He is a faculty member (Privatdozent) in the Department of Computer Science at Saarland University and contributes to the Saarland Informatics Campus. His work bridges symbolic computation, logic, and applications in systems biology and engineering. Education: Habilitation in Informatics, Universität Passau, Germany, 2005 Dr. rer. nat. (Ph.D.), Universität Passau, Germany, 2000 Sturm's research focuses on exact and efficient computation, computer algebra, logic, and formal reasoning. Key areas include quantifier elimination, decision procedures, tropical geometry, and their application to chemical reaction networks and systems biology. He develops methods used in SMT solving and mathematical biology. His work emphasizes algorithmic reduction of biological models with multiple time scales and symbolic analysis of dynamical systems. His recent publications reflect a strong trend in applying symbolic computation to biological networks, particularly using real algebraic geometry, tropical methods, and logic-based approaches to analyze steady states, binomiality, and toricity in reaction systems. He integrates formal reasoning with model reduction and conservation laws, contributing to both theoretical foundations and practical software tools. Scientific Awards: Open Source Excellence Award by SourceForge for REDUCE/Redlog Sturm actively advises and collaborates with researchers in interdisciplinary projects. He has led major grants such as SYMBIONT (ANR/DFG) and SC² (EU H2020), involving teams across Europe. He is Editor-in-Chief of Mathematics in Computer Science (Springer) and associate editor of the Journal of Symbolic Computation . His leadership extends to software development, including Redlog and ODEbase, which support symbolic reasoning and biomodel sharing. Labs and Teams: He leads or has led research groups in arithmetic reasoning at MPI Informatics and participates in the Automation of Logic department. He is central to the SC² community, fostering collaboration between satisfiability checking and symbolic computation.
Yu-Fang Chen is a Full Professor and Research Fellow at the Institute of Information Science, Academia Sinica, Taiwan, where he has been affiliated since 2018. His research group focuses on cutting-edge work in formal methods, quantum programming, and automata theory, with significant contributions to quantum circuit verification and constraint solving. His research centers on developing automata-based frameworks for quantum program verification (AutoQ Project), string constraint solving (Z3-Noodler), and symbolic execution techniques. Core interests include formal verification of quantum systems, satisfiability modulo theories, automata theory applications in quantum contexts, and developing practical verification tools. Chen's recent publications (2020-2025) demonstrate a strong focus on quantum circuit verification, automata theory adaptations for quantum systems, and string constraint solving. Work frequently combines theoretical foundations with practical tool development, showing consistent innovation in quantum program analysis techniques and symbolic execution methods. Awards & Honors: Academia Sinica Scholar Award (2025-2029) SIGLOG/CACM research highlights nomination (2025) Distinguished Paper Awards (OOPSLA 2023, PLDI 2023) Best Paper Awards (FM 2023, TACAS 2010) Young Scholar Creativity Award (2023) MOST Research Project for Excellent Junior Research Investigators (2020-2023) Chen actively advises PhD students and postdoctoral researchers, with open positions advertised for his quantum computing and formal methods research group. He leads significant projects including the AutoQ framework development and has secured multi-year funding through the Academia Sinica Scholar Award and MOST grants. He directs a research laboratory at Academia Sinica focused on automata theory and quantum verification, developing tools like AutoQ and Z3-Noodler. The team collaborates internationally and regularly contributes to top-tier conferences in formal methods and programming languages.
Cesare Tinelli is the F. Wendell Miller Professor of Computer Science at the University of Iowa within the College of Liberal Arts and Sciences. He is a co-director of the Computational Logic Center and leads the development of critical tools like the CVC4 and cvc5 SMT solvers, as well as the Kind model checker. His academic credentials include: Ph.D. in Computer Science (1999), University of Illinois at Urbana-Champaign M.S. in Computer Science (1995), University of Illinois at Urbana-Champaign Laurea in Scienze dell'Informazione (1990), University of Bari Research Interests : Tinelli specializes in Automated Reasoning , particularly Satisfiability Modulo Theories (SMT) , Model Checking , Software Verification , and Formal Methods . His recent work explores Inductive Reasoning in SMT , Proof-Certificate Generation , and Logical Frameworks for Proof Systems . His methodologies bridge theoretical advancements with practical implementations, impacting both academia and industry. Scientific Contributions : Tinelli's research drives innovation in SMT solving, model checking, and automated theorem proving. His 15 most recent publications span topics from stateful protocol testing ( Saecred ) to proof certification ( IsaRare ) and generalized optimization ( Generalized OMT ). Awards and Recognition : NSF CAREER Award (2003) Haifa Verification Conference Award (2010) CAV Award (2021) Advising and Collaborations : His former students and postdocs hold positions at leading institutions like NASA, Intel, MIT, and EPFL. He collaborates with organizations such as Amazon, Facebook, General Electric, and Microsoft.
Ilkka Niemelä is a Professor of Computer Science at Aalto University's School of Science. He has held leadership roles including Head of the Laboratory for Theoretical Computer Science at Helsinki University of Technology, Chair of the Degree Program in Computer Science and Engineering, and Dean of Aalto University's School of Science. His research focuses on automated reasoning and constraint programming for solving computational problems. His work spans key areas in computational logic, including answer-set programming, non-monotonic reasoning, bounded model checking, and parity reasoning. He has explored applications in formal verification, optimization, and system design, with publications reflecting interdisciplinary contributions to artificial intelligence and theoretical computer science. Scientific awards and honors include: Superior of the year at Helsinki University of Technology (2007) Annual dissertation award from the Finnish Society for Computer Science (1993) Knight, First Class, of the Order of the White Rose of Finland (2015) 20 Year Test of Time Paper Award (2016) EurAI Fellow (2013) His research group has pioneered methods in answer-set programming and bounded model checking, with recent publications addressing program transformations, timed automata, and parity games. Niemelä has also served in administrative roles such as Vice President and Provost at Aalto University, contributing to academic governance and education.
Alessandro Gianola is a Tenure Track Assistant Professor at the Department of Computer Engineering, College of Engineering, University of Lisbon, and a Senior Researcher at INESC-ID. He earned a PhD in Computer Science cum laude from the Free University of Bozen-Bolzano. Research Focus: Business Process Management, formal methods, AI verification of data-aware processes, multi-perspective process mining, and constraint-based reasoning. Awards: ECAI 2024 Outstanding PC Member, 2024 INESC-ID Best Young Researcher, 2023 CADE Bill McCune PhD Award, and multiple best paper awards. Education: PhD in Computer Science (Free University of Bozen-Bolzano, 2022). His recent publications analyze data-aware processes using SMT techniques, with applications in conformance checking, model checking, and formal verification. He leads projects like FCT OptiGov and INESC-ID eProcess. Conference Leadership: PC Co-chair for EDOC 2025, Workshops Co-chair for FLoC 2026, and co-chair for multiple FM-BPM workshops. Research Groups: ELLIS, LUMLIS, ARSR, OVERLAY, and former KRDB Research Centre.
Ahmed Rezine is a Senior Lecturer and Associate Professor at the Department of Computer Science (IDA) , specifically within the Software and Systems (SAS) division at Linköping University . His research focuses on software verification , machine learning , and cybersecurity , particularly in the context of deep neural networks and embedded systems . Research Trends: His recent publications, such as VNN: Verification-Friendly Neural Networks (2024) and Trojans in Instruction Sets (2024), highlight his work at the intersection of AI robustness and hardware security . Earlier studies (2023-2017) emphasize formal verification of concurrent systems and GPU architectures , reflecting a consistent focus on parameterized systems and security analysis . Colleagues & Collaborations: Rezine collaborates with researchers in the Software and Systems group, part of the Wallenberg Autonomous Systems Program (WASP) . His work intersects with AI IDA and Embedded Systems (ESLAB) , focusing on autonomous systems and real-time processing .
Hans-Jörg Schurr is a postdoctoral researcher in Computer Science at the University of Iowa's College of Engineering, focusing on SMT solving and formal verification. He contributes to the cvc5 SMT solver and leads development of the SMT-LIB benchmark library alongside Clark Barrett, Mathias Preiner, and Pascal Fontaine. Research Focus: Proof certificates, logical frameworks, and expressive type systems for SMT solvers Tools: Eunoia language (combining LFSC and Alethe), veriT SMT solver Collaborations: Active with the Alethe proof format specification team and SMT competition organizers Scientific Awards: Best Paper by a Junior Researcher (PxTP 2021) Teaching: Provided lectures at University of Iowa (Programming Language Concepts, Logic in Computer Science, Algorithms) and Polytech Nancy (Software Engineering, Distributed Programming). Recognized by graduating class of 2023 and received Thank-a-Teacher Letter.
Dirk Beyer is a Full Professor and Head of Research Chair at the Department of Computer Science, Ludwig-Maximilians-Universität München (LMU Munich), where he leads the Software and Computational Systems Lab. His research focuses on developing models, algorithms, and tools for constructing and analyzing reliable software systems, with emphasis on software verification, model checking, and static analysis. Professor Beyer's research spans multiple critical areas in software engineering and formal methods. He has made significant contributions to software model checking through tools like CPAchecker and BLAST, structure analysis of large systems using CrocoPat and CCVisu, and formal verification of real-time systems with Rabbit. His work on interfaces for component-based design (Chic) has advanced modular software development approaches. Beyer has pioneered methodologies in benchmarking and reliable experimental evaluation through BenchExec, which has become a standard in tool competitions. Analysis of his recent publications reveals a strong focus on advancing software verification techniques, particularly in transferring knowledge between hardware and software verification domains, decomposing verification tasks for parallel processing, and improving the effectiveness of verification witnesses. His work consistently bridges theoretical foundations with practical tool implementations, with a growing emphasis on comparative evaluation and competition frameworks that drive the field forward. ACM SIGSOFT Distinguished Paper Award (FSE 2024) ACM SIGSOFT Best Artifact Award (FSE 2024) As a principal investigator of the DFG Research Training Group ConVeY, Beyer has secured significant funding for advancing verification techniques. He has played leadership roles in numerous software verification competitions including SV-COMP and Test-Comp, serving as PC Chair for major conferences like TACAS 2018 and VMCAI 2020. His service contributions extend to chairing ETAPS 2022 and organizing multiple workshops on CPAchecker. Professor Beyer leads the Software and Computational Systems Lab at LMU Munich, which has developed numerous influential verification tools including CPAchecker (configurable software verification), BenchExec (reliable benchmarking), and CCVisu (software structure visualization). The lab maintains active collaborations with research groups worldwide and contributes significantly to the international verification community through competitions, benchmarks, and open-source tool development.
Cayden Codel is a Researcher at Carnegie Mellon University's Computer Science Department , focusing on programming languages and formal verification. His work bridges theoretical logic with practical applications in automated reasoning and constraint solving. Research Interests: Programming Languages, Formal Verification, Satisfiability (SAT) Solvers, Satisfiability Modulo Theories (SMT), Automated Theorem Proving, Machine Learning Institution: Carnegie Mellon University (CMU) His publications emphasize formal verification for logical systems, SMT/SAT solvers , and reinforcement learning applications. Articles from 2024-2019 reveal a trajectory from foundational logic to real-world dataset design (e.g., Minecraft-based AI research). Thesis Advisors: Marijn Heule, Jeremy Avigad Contact: ccodel@andrew.cmu.edu
Byron Cook is a Professor of Computer Science at University College London (UCL) and Vice President & Distinguished Scientist at Amazon / AWS . His work bridges formal methods , automated reasoning , and program verification in domains spanning GenAI , distributed systems , hardware , operating systems , and biological systems . Academic Roles : UCL Professor (since 2014), Microsoft Researcher (2004-2014) Industry Leadership : Amazon (2018-present), Microsoft (1999-2014) Research Interests focus on theoretical computer science with applications in: Program Termination Proving (TERMINATOR/T2 tools) Memory Safety (SLAyer project) Biological Systems Modeling (Bio Model Analyzer) Cloud Security (AWS Access Analyzer, Tiros) Formal Verification of Windows device drivers (Static Driver Verifier) Scientific Contributions include groundbreaking work on automated termination proofs , shape analysis , and access policy verification . His 15 recent publications (2016-2023) demonstrate sustained impact in formal verification of AWS systems , biological modeling , and distributed SMT solving . PhD Students Advised : Alexey Gotsman, Eric Koskinen Current PhD Student : Kaustubh Nimkar Awards : Fellow of the Royal Academy of Engineering (FREng)
Jussi Rintanen is an Associate Professor at the Department of Computer Science , Aalto University . He is an internationally leading researcher in constraint-based planning and decision-making , with a focus on applying AI technologies to automating software production and synthesis of intelligent systems . Helsinki University of Technology (Doctoral Degree, 1997) Albert-Ludwigs-University Freiburg (Venia Legendi, 2005) National ICT Australia / Australian National University (Academic Positions) His research spans automated planning , SAT solving , temporal planning , and constraint-based search methods . Recent work highlights symmetry-breaking constraints , partial observability planning , and acyclicity encodings in SAT frameworks. The 15 most recent articles reflect trends in AI planning , graph algorithms , and formal verification , with applications in software synthesis , temporal reasoning , and uncertainty handling . His methodologies integrate integer programming , SMT encodings , and propositional logic .
Allison Sullivan is an Assistant Professor of Computer Science at The University of Texas at Arlington (UTA), affiliated with the Software Engineering Research Center (SERC) and the College of Engineering. She holds a PhD in Software Engineering from The University of Texas at Austin (2017) and previously served as an Assistant Professor at North Carolina A&T State University (2018-2020). Her research focuses on software reliability through automated engineering techniques and formal methods, supported by NSF and DoD grants. Education: PhD in Software Engineering (UT Austin, 2017), MS (UT Austin, 2014), BS (UT Dallas, 2012). Research interests include automated test generation, mutation testing, program synthesis, and formal verification of autonomous systems. Key areas span Model-Based Testing, First-Order Logic, and SAT/SMT solvers. Publications reflect her work in Alloy-based tools (e.g., AUnit, MuAlloy), mutation testing frameworks, and educational outreach. Notable awards include NSF CAREER (2024), UTA Rising Star (2024), and Outstanding Early Career Faculty (2025). She advises multiple graduate and undergraduate students, teaches courses in algorithms, software testing, and formal methods, and serves on program committees for conferences like ASE, MODELS, and ISSRE. Her broader impacts include K-12 outreach, curriculum development, and mentoring through initiatives like Google Faculty In Residence and AMIE Design Challenge. Labs/Teams: Leads the SCOPE lab at UTA, focusing on program correctness verification.
Dr Martin Nyx Brain is a researcher at City St George's, University of London, affiliated with the Department of Computing within the College of Engineering, Science and Technology. His work focuses on advancing automated reasoning and formal verification techniques for ensuring software safety and security, particularly in critical low-level and embedded systems. His research spans core areas in formal methods, including the development and application of SAT and SMT solvers. He is a co-author of the SMT-LIB standard for floating-point arithmetic and has contributed to the CVC4 solver's floating-point theory, demonstrating deep expertise in logical foundations and solver technology. He applies abstract interpretation, symbolic execution, and deductive verification to analyze systems written in C, C++, and Ada, using tools such as SPARK and CBMC/CPROVER. Dr Brain’s work bridges theoretical logic and practical software verification, with strong relevance to cybersecurity and safety-critical systems. His research interests include formal verification, static analysis, programming language semantics, and automated theorem proving. While no specific publications or awards are listed in the provided text, his technical contributions suggest an active research trajectory in the intersection of programming languages, logic, and software reliability. He is involved in tool development and standardization efforts that are influential in the formal methods community. There is no mention of student supervision, grants, or educational background in the available information. However, his role implies engagement with research teams or labs focused on software verification and automated reasoning, potentially contributing to collaborative projects in formal methods and secure systems engineering.
Yuliya Lierler is a full Professor of Computer Science at the University of Nebraska Omaha (UNO), affiliated with the College of Information Science & Technology (IS&T). She holds the Cheryl Prewett Diamond Professorship since 2020 and received the Mentor of the Year Award in 2025. Her research focuses on artificial intelligence, particularly knowledge representation, automated reasoning, declarative problem solving, and natural language understanding. She co-directs the NLPKR lab and has authored over 70 peer-reviewed articles in top AI venues. Her books include Discrete Mathematics in a Nutshell and Digital Minimalism for Teens . Education: Ph.D. in Computer Science from the University of Texas at Austin (2010). Professional development includes training in AI-driven teaching methodologies and online education. Research Interests: She explores formal methods in AI, including logic programming semantics (e.g., Answer Set Programming), automated reasoning techniques, and applications in natural language processing. Her work bridges theoretical foundations with practical tools, such as the text2ALM information extraction system. Service & Leadership: Co-Chair of the 38th International Conference on Logic Programming (2022), Executive Committee member of the Association for Logic Programming (since 2020), and former Graduate Program Committee Chair (2018–2020). She has organized multiple international conferences and contributed to AI education initiatives. Awards: Recipient of the 2025 Mentor of the Year Award (Nebraska Women in Tech), 2024 Outstanding Research Award (IS&T College), and 2016 Best Student Paper Award (with Amelia Harrison). Labs & Teams: Co-director of the NLPKR lab, focusing on natural language processing and knowledge representation. Collaborates on projects integrating declarative programming with semantic understanding.
