Find Academic Supervisors

Sanjit A. SeshiaView profile

Professor

• Formal Methods
• Cyber-Physical Systems
• Computer Security
• +10 more

Sanjit A. Seshia is the Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley . He is affiliated with the Group in Logic and the Methodology of Science and participates in centers like the Industrial Cyber-Physical Systems Center , Berkeley AI Research , and the Simons Institute for the Theory of Computing . Research interests include formal methods for automated verification and synthesis of dependable systems, with applications to cyber-physical systems , AI-based autonomy , and computer security . His work spans SMT solving, model counting, syntax-guided synthesis, and algorithmic improvisation, with tools like UCLID5 , VerifAI , and Scenic for verifying autonomous systems and educational platforms like CPSGrader . Students and collaborators include notable researchers such as Dorsa Sadigh (Stanford), Daniel Fremont (UC Santa Cruz), and Hazem Torfah (Chalmers). He has co-founded startups like Decyphir and 20ⁿ Labs based on his research.

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.

Vijay GaneshView profile

Professor

• SAT/SMT Solvers
• Artificial Intelligence
• Formal Methods
• +5 more

Dr. Vijay Ganesh is a Professor of Computer Science at Georgia Institute of Technology, where he also serves as Associate Director of the IDEaS Institute and is affiliated with Tech AI. Previously, he held roles as Associate Professor (2018–2023) and Assistant Professor (2012–2018) at the University of Waterloo, and Research Scientist at MIT (2007–2012). He earned his PhD from Stanford University in 2007. His research focuses on SAT/SMT solvers and their applications in AI, software engineering, security, mathematics, and physics. Notable contributions include developing solvers like MapleSAT, Z3str4, and AlphaZ3, and exploring machine learning-augmented reasoning. He has led projects in logic for AI, proof complexity, and security of blockchain technologies. His awards include ACM Impact Paper (2019), ACM Test of Time (2016), and DATE’s Ten-Year Most Influential Paper (2008). He has advised startups like Quantstamp, a blockchain security firm, and co-directed the Waterloo AI Institute (2021–2023). His teaching includes courses on discrete mathematics, software engineering, and AI. Education: PhD in Computer Science, Stanford University (2007); Master’s in Electrical Engineering, Stanford (2000) Research Interests: SAT/SMT solvers, formal methods, automated testing, AI security, combinatorial mathematics Affiliations: Georgia Tech’s School of Computer Science, IDEaS Institute

Cezary KaliszykView profile

Professor

• Theoretical Computer Science
• Automated Reasoning
• Formal Methods
• +13 more

Cezary Kaliszyk is a Professor in Theoretical Computer Science at the University of Melbourne. His research focuses on automated reasoning, formal methods, and learning for reasoning, particularly in the context of interactive theorem proving and formalized mathematics. He leads the ERC project 'FormalWeb3' and has been involved in several other significant research initiatives. Theoretical Computer Science Automated Reasoning Formal Methods Interactive Theorem Proving Machine Learning for Theorem Proving Formalized Mathematics Proof Guidance Learning for Reasoning His research explores the integration of machine learning techniques with formal reasoning systems to enhance automation in theorem proving. This includes developing systems like CoqHammer and Tactician, advancing premise selection, proof guidance, and learning-based proof search strategies. His work bridges logical foundations with practical AI-driven tools for formal verification. The recent publications demonstrate a consistent focus on advancing automated and interactive theorem proving through learning techniques, formalization of mathematical concepts (like surreal numbers), and improving reasoning systems (e.g., Prover9, tableaux methods). There is a strong emphasis on practical system development, formalization projects, and learning-based enhancements to reasoning. ERC project 'FormalWeb3' - Principal Investigator Cost Action EuroProofNet - WG5 Leader until 2024 FWF project P26201 - developing HOL(y)Hammer Other projects: JSPS P10044, NWO MathWiki, SURF WebDed, ProofWeb He has advised several PhD students to completion, including Michael Färber, Thibault Gauthier, Yutaka Nagashima, Stanisław Purgał, and Liao Zhang, and is currently supervising Daniel Ranalter and Neil Vyas. He has not received any explicitly mentioned scientific awards in the provided text. His work involves leadership in collaborative systems such as ProofWeb and HOL Import, and participation in major formalization efforts including the Mizar library integration with Isabelle. He is actively involved in the development of tool ecosystems for formal mathematics and automated reasoning.

Laura KovacsView profile

Professor

• Automated Reasoning
• Program Analysis
• Symbolic Summation
• +5 more

Laura Kovacs is a full Professor at TU Wien's Faculty of Informatics, where she serves as head of the FORSYTE research unit focused on Automated Program Reasoning. She also holds a part-time associate professorship at Chalmers University of Technology in Sweden. As a leading researcher in automated reasoning, she was recently elected President and Chair of the ETAPS steering committee (2025) and has received prestigious awards including ERC Consolidator and Starting Grants. TU Wien, Faculty of Informatics (2016-present) Chalmers University of Technology, Sweden (part-time) Postdoctoral researcher at EPFL and ETH Zurich (2007-2010) FWF Hertha Firnberg Research Fellow (2010-2013) Her research spans automated theorem proving, program analysis, symbolic summation, and computer algebra, with a particular focus on developing theoretical foundations and practical tools for software verification. She is best known as co-developer of the Vampire theorem prover, which recently made history by winning all eight divisions at the CASC competition in 2025. Her recent publications demonstrate strong activity in first-order reasoning, quantifier handling, and security applications, with notable work including the Amazon-funded FOREST project (2020) and QuAT (2023). The 2025 CAV conference awarded her co-authored paper 'The Vampire Diary' a Distinguished Paper Award, highlighting continued leadership in the field. ERC Consolidator Grant 2020 for 'ARTIST: Automated Reasoning with Theories and Induction for Software Technology' Wallenberg Academy Fellowship (2014) ERC Starting Grant (2014) Amazon Research Awards (2020, 2023) Distinguished Paper Award at CAV 2025 Professor Kovacs actively supervises PhD students working on cutting-edge topics in automated reasoning, with recent successful defenses including Márton Hajdu's 'Redundancy, Rewriting, and Induction' (2025) and Sophie Rain's 'Automated Security Analysis of Blockchain Protocols' (2025). She leads the newly established Doctoral College on Automated Reasoning at TU Wien, which received FWF funding for 13 doctoral positions focusing on security and AI applications. As head of FORSYTE, she oversees research in automated program reasoning, working closely with colleagues on projects spanning software model checking, static analysis, and formal methods for distributed systems. Her group has established strong industry connections, particularly with Amazon through the Amazon Research Awards program.

• Formal Methods
• Satisfiability (SAT)
• Satisfiability Modulo Theories (SMT)
• +11 more

Enric Rodríguez Carbonell is a faculty member at the Department of Computer Sciences within the Faculty of Computer Science at Universitat Politècnica de Catalunya (UPC). He is a key member of the LOGPROG - Lògica i Programació research group, focusing on formal methods, automated reasoning, and combinatorial optimization. Research Interests: His work centers on satisfiability (SAT), satisfiability modulo theories (SMT), and their applications in program verification, constraint solving, and optimization. He investigates techniques such as conflict-driven learning, invariant generation, and Max-SMT for proving termination and safety. His research bridges theoretical foundations with practical applications in software analysis and industrial problem-solving. Publication Trends: His recent publications (2020–2024) show a sustained focus on enhancing SAT and SMT solvers, particularly in pseudo-Boolean reasoning, integer linear programming, and multi-conflict analysis. Earlier works established contributions in non-linear arithmetic, termination proofs, and efficient encodings for cardinality constraints, reflecting a long-term commitment to foundational and applied aspects of automated reasoning. Scientific Awards: Best student paper award at SAT 2024 Advising and Grants: Rodríguez Carbonell has contributed to multiple competitive R+D+i projects under Spain’s State Research Plans, indicating active grant involvement. He has co-authored doctoral theses and educational initiatives like Jutge.org, demonstrating engagement in academic supervision and pedagogical innovation. Labs and Teams: He is a core researcher in the LOGPROG group at UPC, which specializes in logic and programming, with strong collaborations across formal methods, verification, and constraint technologies.

Alan HuView profile

Professor

• Formal Verification
• Algorithms
• Computer Architecture
• +3 more

Alan Hu is a Professor in the Department of Computer Science at the University of British Columbia (UBC), part of the Faculty of Science. His research focuses on formal verification, algorithms, computer architecture, and electronic design automation. He teaches courses such as Intermediate Algorithm Design and Analysis (CPSC 320) and Introduction to Formal Verification and Analysis (CPSC 513). Dr. Hu has received notable awards, including the IEEE Council on Electronic Design Automation Outstanding Service Award and the IBM Faculty Award. His work emphasizes scalable verification techniques, SAT-based algorithms, and optimization in cloud computing and hardware systems. His research spans formal methods for hardware/software systems, including verification of embedded software, cache coherence, and network function virtualization. Notable contributions include advancements in SAT modulo theories, data race detection in heterogeneous systems, and cloud resource allocation frameworks like Cospot. Dr. Hu has been actively involved in teaching and curriculum development, consistently offering courses on algorithms, formal verification, and software design since 2000. His publications reflect a blend of theoretical foundations and practical applications in electronic design, cloud infrastructure, and verification tools. His scientific achievements include innovations in post-silicon validation, emulation-based coverage reduction, and formal analysis for debug trace optimization. He also contributes to the academic community through conference organization and editorial roles in formal verification and computer-aided design.

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.

Konstantin KorovinView profile

Associate Professor

• Automated Theorem Proving
• Formal Methods
• Verification
• +3 more

Konstantin Korovin is an Associate Professor and Reader in Formal Methods at the University of Manchester. He leads the Formal Methods Research Group and is a core developer of the iProver theorem prover, a tool for automated reasoning in first-order logic with applications to verification, neuro-symbolic systems, and machine learning integration. His work focuses on combining automated reasoning techniques with machine learning, particularly in areas like premise selection, neural architecture for term synthesis, and hybrid verification systems. Affiliations: Centre for Digital Trust and Society, SCorCH Project (Secure Code for Capability Hardware) Research Beacons: Digital Futures Key research interests include automated theorem proving, verification of machine learning models, non-linear constraint solving, and neuro-symbolic reasoning. He has contributed to tools like ESBMC (for C++ program verification) and SMLP (a symbolic machine learning prover). His work spans theoretical advancements in superposition calculus and practical applications in hardware verification and systems biology. Collaborations include projects on DNA-based computing, robotic scientific discovery (e.g., Genesis), and formal methods for industrial hardware verification. Korovin’s research is supported by grants from the Engineering and Physical Sciences Research Council (EPSRC) and industry partnerships.

Martin BrombergerView profile

Researcher

• Automated Reasoning
• Theorem Proving
• Linear Arithmetic
• +3 more

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.

Yu-Fang ChenView profile

Professor

• Formal Verification
• Quantum Programming
• Automata Theory
• +3 more

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 TinelliView profile

Professor

• Automated Reasoning
• Satisfiability Modulo Theories (SMT)
• Model Checking
• +7 more

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.

Alessandro GianolaView profile

Assistant Professor

• Formal Verification
• Business Process Management (BPM)
• Automated Reasoning
• +6 more

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.

Cayden CodelView profile

Researcher

• Programming Languages
• Formal Verification
• Satisfiability (SAT) Solvers
• +3 more

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

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