Find Academic Supervisors

Ruben MartinsView profile

Assistant Professor

• Constraint Programming
• Program Synthesis
• Formal Verification
• +3 more

Ruben Martins is an Assistant Professor at Carnegie Mellon University's School of Computer Science and serves as the program director of the Master of Science in Computer Science (MSCS) . His research focuses on the intersection of constraint programming, program synthesis, analysis, and verification, with recent work aiming to make formal methods tools more accessible through automated reasoning. Ruben earned his Ph.D. with honors from the Technical University of Lisbon, Portugal (2013) , followed by postdoctoral research at the University of Oxford (2014-2015) and UT Austin (2015-2017) . Research Interests : Ruben's work bridges constraint programming and program synthesis , with applications in software verification , optimization , and automated reasoning . He has developed award-winning tools like Open-WBO , a modular MaxSAT solver that has won gold medals in international competitions. His publications span top-tier venues such as POPL , PLDI , FSE , SAT , and CP , often addressing real-world challenges from program analysis to network security. Scientific Awards include: Distinguished Paper Award at PLDI 2018 Distinguished Paper Award at FSE 2021 Distinguished Paper Award at SAT 2022 Gold medals for Open-WBO in MaxSAT competitions Teaching & Advising : Ruben mentors Ph.D., Master’s, and undergraduate students in research projects related to program synthesis, formal methods, and constraint solving. He teaches courses such as Bug Catching: Automated Program Verification and Advanced Topics in Logic: Automated Reasoning and Satisfiability , emphasizing hands-on experience with tools like Why3. His advising spans topics from AI-driven program repair to network protocol verification , fostering collaboration across disciplines.

Jürgen GieslView profile

Professor

• Program Verification
• Automated Deduction
• Termination Analysis
• +12 more

Jürgen Giesl is a Professor at the Teaching and Research Area Computer Science 2 within the Department of Computer Science at RWTH Aachen University , Germany. He leads research in programming languages, formal verification, automated deduction, and term rewriting systems. Research Interests: Automated Termination and Complexity Analysis of Programs Dependency Pairs and Term Rewriting Systems Verification of Probabilistic and Integer Programs Static Analysis and Symbolic Execution Model Checking and Constrained Horn Clauses Development of Automated Tools (AProVE, LoAT) His recent research, reflected in the latest publications, focuses on termination and complexity analysis for probabilistic programs, polynomial loops, and integer programs, using advanced techniques such as dependency pairs, loop acceleration, and semiring semantics. He also contributes to SMT solving and transitive relation learning for infinite-state model checking. Scientific Awards: Best Tool Paper Award at iFM 2017 Silver Medal (Second Best Paper) at SEFM '16 Best Paper Honourable Mention at IJCAR 2024 Best Student Paper Honourable Mention at IJCAR 2024 Advising and Grants: Giesl has supervised numerous PhD and Master’s students, including prominent researchers such as Fabian Frohn, Jens Hensel, Nils Lommen, and Marcel Hark. He leads a large research group focused on automated verification and has contributed extensively to international verification competitions. His work is supported by ongoing research grants and collaborations with leading institutions in formal methods. Labs and Teams: He leads the Programming Languages and Verification research group at RWTH Aachen, which develops and maintains the AProVE and LoAT tools. These tools are central to automated termination and complexity analysis and are regularly submitted to international competitions such as TERMCOMP and VBS.

Philipp WendlerView profile

Lecturer

• Software Verification
• Formal Methods
• Program Analysis
• +5 more

Philipp Wendler is an academic lecturer in the Department of Computer Science at Ludwig-Maximilians-Universität München (LMU Munich). He is affiliated with the Software and Computational Systems Lab and actively involved in research, teaching, and open-source tool development. As an employee representative in the steering committee of the Institute of Informatics, he contributes to institutional governance. His research focuses on software verification, formal methods, and program analysis. Key projects include CPAchecker (a configurable verification framework) and BenchExec (a benchmarking tool). His work emphasizes practical applications in automated testing, energy-efficient algorithms, and reproducible benchmarking. Publications span topics like interpolation-based model checking, energy measurement tools, and strategies for software verification competitions. He has contributed to advancing predicate analysis, k-induction, and refinement selection techniques. Notable achievements include leading the development of CPAchecker and BenchExec, which are widely used in academic and industrial verification efforts. His research addresses challenges in scalable verification, flaky test analysis, and energy-aware computing.

Nian-Ze LeeView profile

Assistant Professor

• Formal Methods
• Model Checking
• Program Analysis
• +5 more

Nian-Ze Lee is an Assistant Professor at the Department of Electrical Engineering, College of Electrical Engineering and Computer Science, National Taiwan University, Taiwan, where they lead the Formal Methods and Analysis for Computing and Engineering Laboratory (ForMACE Lab). Additionally, Lee holds a position as a Gastprofessor (Guest Professor) affiliated with the Software and Computational Systems Lab (SoSy-Lab) at LMU Munich, Germany. Lee's research focuses on formal methods, with particular expertise in model checking, program analysis, and electronic design automation. Their work bridges hardware and software verification, developing techniques that transfer methodologies between these domains. A significant portion of their research involves stochastic Boolean satisfiability and threshold logic circuits, with applications in both hardware and software verification. Lee's recent publications demonstrate a strong trend toward developing cross-domain verification techniques, particularly focusing on how hardware model checking approaches can be adapted for software verification. Their work on interpolation-based model checking and configurable program analysis has received recognition through multiple best paper and artifact awards at top-tier conferences. ACM SIGSOFT Distinguished Paper Award (FSE 2024) Best Artifact Award (FSE 2024) Distinguished Artifact Award (TACAS 2024) Best Paper Award (SPIN 2024) Lee has secured research funding including a grant from the German Research Foundation (DFG) for the project 'Bridging Hardware and Software Analysis.' They actively maintain several software projects including Btor2C, Btor2-Cert, CPV, MoXIchecker, and contribute to CPAchecker and BenchExec. Lee is currently recruiting Ph.D., Master's, and Bachelor's students to work on formal methods research, with Ph.D. students potentially enrolled at LMU Munich through a DFG-funded project.

Fabio MogaveroView profile

Associate Professor

• Theoretical Computer Science
• Formal Verification
• Temporal Logic
• +12 more

Fabio Mogavero is an Associate Professor in Theoretical Computer Science at the Department of Electrical Engineering and Information Technology, Università degli Studi di Napoli Federico II. His research spans formal specification, verification, and synthesis of systems, with a strong focus on logics, automata, games, and database theory. Ph.D. in Computer Science, Università degli Studi di Napoli Federico II, 2011 M.Eng. in Computer Science Engineering, Università degli Studi di Napoli Federico II, 2007 B.Eng. in Computer Science Engineering, Università degli Studi di Napoli Federico II, 2005 His primary research interests include formal verification, temporal and strategic logics, automata over infinite structures, decidability, and database theory—particularly bag semantics. He has made significant contributions to the theory of parity and mean-payoff games, strategy logic, and SHACL/RDF validation. His recent work explores fragments of first-order and monadic second-order logic, and he actively publishes in top venues such as LICS, ICALP, and IJCAI. The most recent articles highlight a sustained focus on logical characterizations (e.g., automata-theoretic models for temporal logics), game-solving algorithms, and foundational database theory, especially around SHACL and multiset semantics. His work bridges theoretical computer science with practical formal methods. Scientific Awards and Recognition: Erdös number at most 3 (via Erdös → J.H. Spencer → M.Y. Vardi → F. Mogavero) Fabio Mogavero has served on the program committees of major conferences including IJCAI, AAMAS, ECAI, and LICS. He has co-edited proceedings for the Strategic Reasoning (SR) and OVERLAY workshops. He has collaborated with leading researchers such as Moshe Y. Vardi, Orna Kupferman, and Michael Benedikt. He has held postdoctoral and teaching positions at the University of Oxford and Università di Verona. He is actively involved in the theoretical computer science community through conference organization and editorial work. He maintains research collaborations across Europe and the U.S. and continues to contribute to foundational and applied aspects of logic in computer science.

Heribert VollmerView profile

Professor

• Theoretical Computer Science
• Computational Complexity
• Logic in Computer Science
• +6 more

Heribert Vollmer is a Professor of Theoretical Computer Science and Managing Director of the Institute for Theoretical Computer Science at Leibniz University Hannover, where he has been employed since 2002. He is also a member of the Academic Freedom Network and serves as a liaison lecturer for the network at Leibniz University. His extensive academic career includes serving as Dean of Studies for Computer Science from 2015-2023 and as spokesperson for the 'Foundations of Computer Science' department of the German Informatics Society. Professor Vollmer earned his doctorate in 1994 on 'Complexity Classes of Functions' from the University of Würzburg, following studies in computer science with a focus on computational linguistics at the Rhineland-Palatinate University of Education in Koblenz (1984-1989). He completed his habilitation in 2000 with a monograph on 'Some Aspects of the Computational Power of Boolean Circuits of Small Depth' and received a teaching qualification in computer science. His research spans theoretical computer science, computational complexity, and logic, with particular focus on Boolean circuits, complexity classes, and descriptive complexity. He has also made significant contributions to the philosophy of mind and intelligence, exploring the relationship between artificial intelligence and consciousness through the lens of Pierre Teilhard de Chardin's philosophical work. His interdisciplinary approach bridges technical computer science with broader philosophical questions about intelligence in humans and machines. Professor Vollmer's notable recognition includes the Feodor Lynen Fellowship from the Alexander von Humboldt Foundation, which supported his research at the University of California at Santa Barbara. He has published over 140 papers in scientific journals and conference proceedings, authored a textbook on circuit complexity, and edited multiple books in his field. As an academic leader, Professor Vollmer has served as editor of the journal 'ACM Transactions on Computational Logic' and as a member of the editorial board of the 'Yearbook of Academic Freedom.' His research has been supported through various academic positions and fellowships, including his visiting professorship at UC Santa Barbara funded by the Humboldt Foundation. He leads the Institute for Theoretical Computer Science at Leibniz University Hannover and is actively involved in the global computer science community as the German representative to Technical Committee 1 'Foundations of Computer Science' of the International Federation for Information Processing (IFIP).

Christoph WeidenbachView profile

Adjunct Professor

• Automated Deduction
• Decision Procedures
• Theorem Proving
• +5 more

Christoph Weidenbach is an Adjunct Professor in the Computer Science department at Saarland University, Germany, and the head of the research group Automation of Logic at the Max-Planck-Institute for Informatics. His work focuses on automated deduction, decision procedures, and theorem proving, particularly in the context of first-order logic and decidable fragments. He has been actively involved in the development of automated verification tools and techniques, including SAT solvers and SMT frameworks. Education: Diplom (1989), PhD (1996), Habilitation (2000), all in Computer Science at Saarland University. Current Roles: Research Leader (Automation of Logic group, MPI) since 2005; Adjunct Professor (Saarland University) since 2007. Past Roles: Research Coordinator (MPI, 1999-2005); IT Manager (GM Powertrain Europe, 1991-1999). His recent publications highlight trends in automated deduction, formal verification, and constraint solving, with applications in linear arithmetic, network protocols, and semantic web reasoning. He has also contributed to the theoretical foundations of superposition calculi and SCL(FOL) extensions.

Thomas SturmView profile

Academic

• Computer Algebra
• Symbolic Computation
• Real Algebraic Geometry
• +12 more

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.

Hamid BagheriView profile

Associate Professor

• Software Engineering
• Security of Mobile Devices and IoT Systems
• Formal Methods
• +4 more

Hamid Bagheri is an Associate Professor in the School of Computing at the University of Nebraska-Lincoln, where he conducts cutting-edge research at the intersection of software engineering, security, and formal methods. He also serves as a faculty associate of the Institute for Software Research (ISR) at the University of California, Irvine, and co-directs the ESQuaReD Lab (Engineering Software Quality and Reliability through Deductive methods), which focuses on ensuring software quality through rigorous engineering approaches. Dr. Bagheri's research spans several critical areas including security of mobile devices and IoT systems, scaling formal verification with machine learning, software analysis and testing, dependable cyber-physical systems, and automated program repair and fault localization. His work combines theoretical rigor with practical applications, addressing real-world challenges in software security and reliability through publications in top venues like ICSE, FSE, ASE, and IEEE/ACM Transactions journals. His recent publications demonstrate a strong trend toward integrating machine learning techniques with formal methods to enhance software analysis capabilities. This includes leveraging transformers for database design optimization, neuro-symbolic approaches for certified software synthesis, and large language models for repairing formal specifications, reflecting his ability to adapt to emerging technologies while maintaining a strong theoretical foundation. Dr. Bagheri has received numerous prestigious awards including the EPSCoR FIRST Award, the NSF CISE Career Research Initiation Initiative Award, multiple Distinguished Paper Awards from top conferences, and teaching honors such as the SoC Student Choice Outstanding Teaching Award (2023-2024) and the CSE Outstanding Teaching Award (2020-2021). As an advisor, Dr. Bagheri has mentored several successful PhD students including Mohannad Alhanahnah (who joined Chalmers University as a tenure-track faculty member in Fall 2024) and Clay Stevens (who joined Iowa State University as a tenure-track faculty member in Fall 2023). His research has been supported by significant grants from NSF and other funding agencies, with recent work focusing on automated specification repair, security analysis of IoT systems, and verification of network protocols. The ESQuaReD Lab, which Dr. Bagheri co-directs, brings together a multidisciplinary team focused on addressing critical challenges in software quality and reliability through innovative engineering approaches and formal analysis techniques, with applications spanning mobile security, IoT systems, and cyber-physical systems.

Sharon ShohamView profile

Professor

• formal verification
• program analysis
• model checking
• +4 more

Sharon Shoham is a Professor at the School of Computer Science, Tel Aviv University, specializing in formal verification and program analysis. She leads research under a 5-year ERC grant on supervised verification of infinite-state systems and mentors PhD students, postdocs, and visiting scholars. Research Interests : Her work focuses on formal verification, program analysis, model checking, and verification of distributed systems. She explores inductive invariants, quantifier instantiation, and abstract interpretation. Recent Publications (2023-2025) highlight advancements in liveness properties , hyperproperty verification , quantifier elimination , and distributed protocol verification , often leveraging first-order logic and constraint-solving techniques. Scientific Awards : Distinguished paper awards at POPL 2025 and POPL 2024 Best paper and best student paper awards at DISC 2024, CAV 2019, and DISC 2018 Best paper awards at VMCAI 2016, ATVA 2009, SPIN'08, SAS'07, and FMCAD'07 Advising & Grants : Actively recruits strong PhD students and postdocs under an ERC grant. Collaborates with institutions like Technion and Tel Aviv University on verification frameworks and tools such as Ivy and mypyvy.

Bernd FinkbeinerView profile

Professor

• Formal Verification
• Reactive Synthesis
• Hyperproperties
• +4 more

Prof. Bernd Finkbeiner is a faculty member at CISPA Helmholtz Center for Information Security and holds a Professorship in Computer Science at Saarland University. He earned his Ph.D. in 2003 from Stanford University. Leading the Reactive Systems Group since 2003, now part of CISPA, his research focuses on ensuring safety and security in computer systems through formal methods like specification, program synthesis, and verification. Key projects include output-sensitive reactive synthesis (OSARES), hyperproperty logics (HYPER), and real-time monitoring (RTLOLA). Education : Ph.D. in Computer Science, Stanford University, 2003 His research interests span hyperproperties, formal verification, runtime monitoring of cyber-physical systems, and distributed synthesis. He has pioneered tools like StreamLAB and AutoHyper for hyperproperty analysis. His work on temporal causality and information-flow guided synthesis addresses challenges in distributed and secure systems. Key Achievements : Recipient of ERC Advanced Grant 2022–2027 for Project HYPER Best Paper Awards at ICALP 2009, FSEN 2007, and VMCAI 2012 Leader of the Reactive Systems Group at CISPA Grants & Funding : ERC Advanced Grant supporting research on hyperproperties His lab develops cutting-edge tools for formal methods, including BoSy for bounded synthesis and RTLola for runtime verification. Current research explores compositional synthesis, explainable reactive systems, and robust monitoring for medical and autonomous systems.

• Software Model Checking
• Satisfiability Modulo Theories (SMT)
• Craig Interpolation
• +4 more

Alexander Nutz is a Researcher at the University of Freiburg's Department of Computer Science, affiliated with the Software Modeling and Verification Group. His primary research focuses on software model checking, satisfiability modulo theories (SMT), and Craig interpolation. He contributes to the development of verification tools such as SMTInterpol and the Ultimate Program Analysis Framework. Nutz has held teaching roles in courses like Automata Theory, Decision Procedures, and Program Analysis since 2012, collaborating extensively with colleagues on seminar leadership and course assistance. Education: PhD in Computer Science from the University of Freiburg (2019), focusing on 'Data Flow in Program Verification.' Professional activities include jury membership in the SV-COMP competition (2014-2016, 2018) and contributions to the AVACS research project. His work emphasizes program analysis, verification frameworks, and automated reasoning techniques. Research interests span formal methods, program analysis, and the application of SMT solving to real-world systems like smart contracts. Nutz's projects include enhancing verification tools for memory safety checks and integrating data flow graphs into verification processes. Key contributions: Development of Ultimate Kojak and Automizer tools, exploration of map abstraction techniques, and advancements in interpolation-based verification methods. His publications address challenges in non-linear arithmetic verification and automated reasoning for complex software systems.

Florian FrohnView profile

Lecturer

• Program Verification
• Termination Analysis
• Complexity Analysis
• +11 more

Florian Frohn is a tenured lecturer ("Lehrkraft für besondere Aufgaben") in the Programming Languages and Verification research group at the Department of Computer Science, RWTH Aachen University. He holds a Dr. rer. nat. (2018), MSc (2013), and BSc (2011) in Computer Science, all from German institutions, with his bachelor's studies completed part-time. His research interests center on formal methods for software verification, including automated termination and complexity analysis of imperative programs, satisfiability of Constrained Horn Clauses (CHCs), SMT solving with integer exponentiation, loop acceleration, term rewriting systems, and abstract interpretation. He is a key contributor to several influential tools: LoAT (Loop Acceleration Tool), AProVE (Automated Program Verification Environment), and SwInE; he also worked on Astrée and the CAGE toolchain developed under the DARPA STAC program. His recent publications (2023–2024) demonstrate continued leadership in top venues such as FM, IJCAR, FoSSaCS, and SAS, with work advancing loop acceleration, non-termination proofs, and SMT solving. These contributions reflect a strong trend in developing practical, automated techniques for program verification and analysis. IJCAR Best paper honourable mention (2024) EASST Award for best ETAPS paper (2020) iFM Best Tool Paper Award (2017) ISR Best Poster Award (2017) SEFM Recognition Award (2016) CADE Woody Bledsoe Travel Award (2016) Florian Frohn actively contributes to the research community through program committee roles for major workshops and conferences including TACAS, HCVS, WST, SMT, and LPAR. He has advised no listed students but has been involved in mentoring through research collaborations. His teaching portfolio includes courses on verification techniques, satisfiability checking, and advanced programming concepts. He leads the Termination and Complexity Competition (termCOMP) and participates in organizing key events in the formal methods community.

Tim LyonView profile

Researcher

• Computational Logic
• Proof Theory
• Modal Logics
• +3 more

Dr. Tim Lyon serves as a Research Associate within the Computational Logic group at Dresden University of Technology's Faculty of Computer Science. He is actively engaged in the ERC-funded DeciGUT (A Grand Unified Theory of Decidability in Logic-Based Knowledge Representation) project, focusing on theoretical foundations of computational logic. His research centers on computational logic , specializing in proof systems for fragments of first-order logic, non-classical logics, and modal logics. Key contributions include developing sequent-based frameworks for Gödel-Löb provability logic, bi-intuitionistic extensions, and decidability analyses for quasi-dense modal systems. His work bridges theoretical proof theory with practical applications in knowledge representation and automated reasoning. Analysis of his recent publications (2023-2025) reveals a concentrated focus on decidability mechanisms and unified proof-theoretic frameworks . His research spans theoretical investigations (e.g., fixed-point equations in dynamic logic) to applied systems (e.g., standpoint temporal logic for multi-perspective reasoning), demonstrating consistent innovation in sequent calculus applications across diverse logical domains. Dr. Lyon advises master's students through thesis topics such as "A Simplified Tableau Calculus for Standpoint LTL" and "Ill-Founded Linear Nested Sequents for LTL" under the DeciGUT project. His research is supported by European Research Council funding, with collaborative work spanning institutions including Vienna University of Technology, CNRS, and KU Leuven. He operates within the International Center for Computational Logic (ICCL), a specialized research unit under the Faculty of Computer Science dedicated to advancing logical methods in computer science through interdisciplinary collaboration and theoretical innovation.

• Formal Verification
• Hardware Design
• Quantum Computing
• +5 more

Professor Rolf Drechsler is affiliated with the Department of Mathematics and Computer Science at the University of Bremen, where he maintains an active research profile in formal verification, hardware design, and quantum computing. His office is located in the Multi-purpose high-rise building (MZH) 4330, and he can be reached at drechsler@uni-bremen.de or drechsler@informatik.uni-bremen.de. Dr. Drechsler's research focuses on formal verification techniques, particularly polynomial formal verification methods, binary decision diagrams (BDDs), in-memory computing architectures, and quantum circuit verification. His work bridges theoretical computer science with practical hardware implementation challenges. Notably, he has recently explored the integration of large language models (LLMs) with hardware verification and design automation, representing an emerging interdisciplinary research direction. An analysis of his 2024-2025 publications reveals a strong emphasis on verification methodologies for emerging computing paradigms. His research spans quantum computing verification (qSAT, quantum circuit debugging), in-memory computing (MAGIC-based architectures, memristive crossbars), and traditional hardware verification enhanced by AI techniques. The publications show a pattern of addressing verification challenges in novel computing architectures while maintaining theoretical rigor in formal methods. Professor Drechsler has made significant contributions to Binary Decision Diagram optimization, formal verification of arithmetic circuits, and hardware security. His work on polynomial formal verification represents a distinctive research thread that has evolved over recent years, addressing verification challenges for sequential circuits, approximate adders, and multi-valued logic circuits.