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.
Cezary Kaliszyk is a Professor in Theoretical Computer Science at the University of Melbourne, previously affiliated with the University of Innsbruck. He is actively involved in research and leadership in formal methods, automated reasoning, and machine learning for theorem proving. Research Interests: Automated Reasoning and Interactive Theorem Proving Formalized Mathematics and Proof Automation Machine Learning for Logic and Theorem Proving Integration of AI with Proof Assistants (Coq, Isabelle) Dependent Type Theory and Higher-Order Logic His recent publications (2023–2025) span topics in dependently-typed logic, learning for proof guidance, formalization of surreal numbers, and blockchain-based formal methods. The works consistently bridge formal logic with machine learning, emphasizing automation, explainability, and cross-system integration. Scientific Leadership and Projects: Principal Investigator, ERC project FormalWeb3 Lead Developer, CoqHammer , Tactician , ProofWeb WG5 Leader, COST Action EuroProofNet (until 2024) Contributor to HOL(y)Hammer , Isabelle Enigma He supervises multiple PhD students and has mentored several graduates in formal methods and AI. He teaches courses in theoretical computer science, logic, and machine learning. There are no listed awards in the provided data, but his extensive publication record and project leadership indicate significant recognition in the field. Labs and Research Groups: He leads a research group focused on formal methods and learning-based reasoning, collaborating internationally on projects involving proof automation, formal libraries, and semantic technologies.
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.
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.
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
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.
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.
Christopher Lynch is a Professor in the Department of Computer Science at Clarkson University, part of the Coulter School of Engineering & Applied Sciences. His research focuses on Automated Deduction, including theorem proving, algorithm efficiency, and cryptographic protocol analysis. He has contributed to the development of efficient algorithms and tools for verification in hardware/software systems. His research interests include automated deduction, automated reasoning, and theorem proving, with a particular emphasis on improving algorithm efficiency for verifying specifications in hardware and software. He has developed new algorithms and modified existing ones to enhance their performance. Additionally, his work extends to cryptographic protocol analysis, focusing on symbolic methods and tools like CryptoSolve to ensure system security. His recent articles explore advancements in satisfiability modulo theories (SMT), unification algorithms (e.g., XOR unification and asymmetric unification), and the application of formal methods to cryptographic systems. Key contributions include improving theorem proving efficiency and developing tools for protocol verification. Christopher Lynch has been involved in collaborative research grants, including the "Unification Laboratory" projects aimed at enhancing cryptographic protocol analysis tools. No specific grants or advising details beyond this are provided in the text.
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 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.
Scott J. Shapiro is the Charles F. Southmayd Professor of Law and Professor of Philosophy at Yale University, where he bridges legal theory, philosophy, and cutting-edge technology. His work integrates jurisprudence with artificial intelligence, cybersecurity, and international law, establishing him as a leading voice in legal philosophy and AI ethics. He co-founded the Yale Legal AI Lab and served as Special Assistant for AI Ethics at CISA (2024-2025), directly shaping federal cybersecurity policy. Ph.D. in Philosophy, Columbia University (1996) J.D., Yale Law School (1990) B.A. in Philosophy, Columbia University (1987) Shapiro's research centers on the philosophy of law, international criminal law, and the automation of legal reasoning. He pioneers the application of AI to legal systems, exploring how automated reasoning and large language models can formalize and democratize legal processes. His cybersecurity work examines historical hacking incidents to expose systemic vulnerabilities, while his scholarship on international law investigates how the outlawry of war transformed global order. His interdisciplinary approach connects abstract jurisprudence with real-world technological and geopolitical challenges. Recent publications reveal a sharp pivot toward AI-law integration, with 70% of his 2021-2024 work focusing on automated legal reasoning, SMT-based verification, and autonomous agent ethics. Simultaneously, he maintains a robust thread in international law, analyzing war manifestos and treaty impacts through historical-legal lenses. This dual trajectory positions him uniquely at the intersection of technological innovation and foundational legal theory. Amazon Research Award (2022, 2023) New York Times Book Review Editors’ Choice (2017) The Economist Book of the Year (2017) Scribes Book Award (2018) Lionel Gelber Prize shortlist Duke of Westminster shortlist Shapiro directs the Yale Legal AI Lab, which develops tools for automating legal reasoning and has secured significant industry funding including two Amazon Research Awards. His CISA role involved advising on AI ethics frameworks for national infrastructure protection. He also founded the Yale Documentary Project, providing legal support to filmmakers, and co-edits the Stanford Encyclopedia of Philosophy. Current grants focus on LLM-based legal democratization and formalizing FISA through automated reasoning systems. The Yale Legal AI Lab, co-founded by Shapiro, builds practical tools for legal automation while the Yale Documentary Project extends his impact to media. His CISA collaboration connects academic research with federal cybersecurity operations, creating a pipeline from theoretical jurisprudence to national security applications.
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.
Diego Calvanese is a Visiting Professor at Umeå University's Department of Computing Science and holds a full professorship at the Free University of Bozen-Bolzano, Italy. His research focuses on AI for data management, including virtual knowledge graphs (VKG), ontology-based data access (OBDA), and formal methods like description logics. He is part-time at Umeå, balancing roles with his primary position in Italy. Calvanese has received prestigious awards including the AAAI Classic Paper Award (2021), EurAI Fellow (2015), and ACM Fellow (2019). He supervises three doctoral students at Umeå and has authored over 350 publications, with an h-index of 71. His work emphasizes data integration, geospatial systems, and ethical AI applications. Key Roles: Associate Programme Chair (IJCAI 2025), Programme Chair (IJCAI-ECAI 2026), Head of AI for Data Management Research Group Research Interests: Knowledge representation, graph data management, explainable AI, and telemonitoring systems like reCOVeryaID. His research group develops tools like Ontop, a VKG system enabling seamless data access across heterogeneous sources. Current projects include geospatial data integration and temporal OBDA frameworks. Calvanese has served on over 150 program committees and editorial boards, including Artificial Intelligence and JAIR. His work bridges technical advancements with societal impacts, addressing AI's role in healthcare, climate, and democracy.
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 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.
