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.
Supratik Chakraborty serves as the Bajaj Group Chair Professor in the Department of Computer Science and Engineering at Indian Institute of Technology Bombay. He maintains dual affiliations with the Centre for Formal Design and Verification of Software and the Centre for Liberal Education at IIT Bombay, demonstrating his cross-disciplinary engagement. Professor Chakraborty's research spans formal methods with focus on formal verification, rigorous analysis of system models, and automated synthesis of systems from specifications. His work bridges theoretical foundations with practical applications, particularly in developing mathematically provable guarantees for increasingly complex hardware, software, and intelligent systems. Current research interests include constrained counting and sampling, scalable formal verification of software and hardware systems, automated synthesis of programs and circuits, and applications of automata, logic and finite model theory to practical verification challenges. His publication trajectory shows a significant evolution from traditional hardware and software verification toward addressing verification challenges in machine learning and AI systems. Recent work increasingly focuses on interpretability of black-box models, verification of neural networks, and synthesis techniques applicable to intelligent systems. The research demonstrates strong interdisciplinary connections between formal methods, programming languages, and artificial intelligence. IIT Bombay Excellence in Thesis (CSE) Award 2011 (for Bhargav Gulavani's thesis) IIT Bombay Excellence in Thesis (CSE) Award 2017 (for Abhisekh Sankaran's thesis) Best Paper in Algorithms and Architecture track at IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1998 Professor Chakraborty has successfully supervised 11 doctoral students, with research spanning formal verification techniques, Boolean functional synthesis, constrained counting, and applications to hardware and software systems. His students have gone on to positions at major institutions including Microsoft Research, TCS Research, Georgia Tech, and BARC, reflecting the strong industry and academic impact of his mentorship. Current research directions show increasing emphasis on verification challenges posed by machine learning systems and AI. His research group at IIT Bombay, while not explicitly named in the materials, appears to focus on formal methods with strong connections to the Centre for Formal Design and Verification of Software. The group maintains active collaborations with international researchers including Moshe Y. Vardi at Rice University, and has made significant contributions to verification tools like VeriAbs that bridge theoretical advances with practical applications.
Leslie Ann Goldberg is a Senior Research Fellow at St Edmund Hall and Professor of Computer Science at the University of Oxford. She currently serves as Head of the Department of Computer Science (on sabbatical 2025-26) and focuses on foundational problems in Algorithms and Complexity Theory , particularly randomised algorithms for network communication, machine learning, and statistical physics models. Her research includes solving Aldous' 1987 conjecture on backoff protocol instability (with John Lapinskas), developing rigorous mathematical analysis frameworks for algorithmic efficiency, and advancing approximate counting techniques via Markov Chain Monte Carlo methods (with Andreas Galanis and collaborators). Key projects involve graph homomorphisms , Moran process dynamics , and #BIS complexity class analysis. Recent publications (2023-2024) span topics like Sybil defense mechanisms, low-temperature sampling on random graphs, and parameterised subgraph counting modulo 2. Her work demonstrates cross-disciplinary impact in computational biology, statistical physics, and database theory. Scientific Awards include Best Paper Prizes at ICALP 2016, ICALP 2010, and IPEC 2017. She supervises PhD student Paulina Smolarova and collaborates extensively with researchers in Oxford and beyond.
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.
Zachary Kincaid is an Associate Professor in the Department of Computer Science at Princeton University's School of Engineering and Applied Science. His research focuses on program analysis, logic, and programming languages, with an emphasis on making program analysis compositional and robust. He received his PhD from the University of Toronto under the supervision of Azadeh Farzan. His work has been implemented in the Duet program analyzer, and he has an Erdős number of 3. Dr. Kincaid's research interests include: Compositional program analysis techniques Algebraic approaches to program analysis Termination analysis and ranking function synthesis Verification of concurrent and parallel programs Automated reasoning and decision procedures Analysis of numerical programs and loops His recent publications show a strong focus on developing novel techniques for program analysis that bridge theoretical computer science with practical verification tools, particularly in nonlinear analysis, quantified reasoning, and compositional verification. Dr. Kincaid has received research support from ONR grant N00014-19-1-2318 for his work on robust program analysis. He has advised graduate students including: Current: Jake Silverman, Nicolas Koh, Nikhil Pimpalkhare Graduated: Shaowei Zhu (PhD 2024, Researcher at Amazon), Charlie Murphy (PhD 2023, Postdoc at University of Wisconsin–Madison) Dr. Kincaid teaches courses including: COS 320 – Compiling Techniques (Spring 2024, 2022, 2020, 2019) COS 516 / ELE 516 – Automated Reasoning about Software (Fall 2025, 2022, 2018) COS 217 – Introduction to Programming Systems (Fall 2024) COS IW – Practical Solutions to Intractable Problems (Fall 2023, Spring 2023, 2018, 2017) COS IW – Little Languages (Spring 2018) COS 597D – Reasoning about concurrent systems (Fall 2016)
Todd Millstein is a Professor in the Computer Science Department at the University of California, Los Angeles (UCLA). He served as the Computer Science Department Chair from 2022-2025 and is also an Amazon Scholar. His research focuses on making software systems more reliable through programming languages techniques, with significant contributions to network verification and probabilistic programming. Millstein received his Ph.D. from the University of Washington Department of Computer Science, where he was a member of the Cecil group led by Craig Chambers. Prior to that, he completed his undergraduate studies at Brown University under the guidance of Paris Kanellakis and Pascal Van Hentenryck. Millstein's research spans several areas of programming languages and systems with a focus on reliability. He has made significant contributions to network verification, developing the Batfish network configuration analyzer which is now managed by Amazon Web Services and forms the basis of Oracle Cloud's Network Path Analyzer. His work has been recognized with the ACM SIGCOMM Networking Systems Award in 2025. He also works on interactive program verification through lemma synthesis and scalable reasoning methods for probabilistic programming languages. His research bridges programming languages theory with practical systems challenges, as highlighted in his SPLASH/OOPSLA 2024 keynote "Everything is a Program (even if it's not)". Millstein's recent publications demonstrate a consistent focus on verification and reliability across multiple domains. His work shows a progression from foundational programming language techniques to practical applications in networking and probabilistic systems. Key themes include data-driven approaches to program analysis, synthesis of verification artifacts, and applying programming languages techniques to non-traditional domains like network configuration. Millstein's scientific achievements have been recognized with numerous prestigious awards including an NSF CAREER Award, an ACM SIGPLAN Most Influential PLDI Paper Award, an ACM SIGCOMM Networking Systems Award, IEEE Micro Top Picks selection, best-paper awards from PLDI, OOPSLA, and SIGCOMM, a Microsoft Research Outstanding Collaborator Award, an Okawa Foundation Research Grant, an IBM Faculty Award, and a Facebook Research Award. He has also received both the Northrop Grumman Excellence in Teaching Award (for junior faculty) and the Eon Instrumentation Inc. Excellence in Teaching Award (for senior faculty) from UCLA Engineering. Millstein advises several Ph.D. students including Ana Brendel, Poorva Garg (co-advised with Guy Van den Broeck), Rajdeep Mondal (co-advised with George Varghese), and Rathin Singha (co-advised with George Varghese). His research has been supported by various grants including an NSF CAREER Award, Okawa Foundation Research Grant, IBM Faculty Award, and Facebook Research Award. He has also been a Co-Founder and Chief Scientist of Intentionet, which was later acquired by Amazon Web Services. Millstein is actively involved in the Batfish project, an open-source network configuration analyzer that has had significant practical impact. Batfish is now managed by AWS, powers Oracle Cloud's Network Path Analyzer, and is used by dozens of companies. His research group continues to work on network reliability, developing techniques for scalable BGP policy verification and behavioral testing of protocol implementations.
Giles Reger is a Senior Lecturer in the Formal Methods Group of the School of Computer Science at the University of Manchester. He completed his BA in Computer Science at the University of Cambridge in 2009, followed by an MSc in Advanced Computer Science at the University of Manchester in 2010 (awarded Highest Achiever of the Year), and earned his PhD from the University of Manchester in 2014 with a thesis titled "Automata based monitoring and mining of execution traces". His research spans several key areas within computer science: Automated Theorem Proving (first-order) Saturation-based techniques Reasoning with theories and quantifiers Finite Model finding Collaborative and Concurrent proof attempts Runtime Monitoring/Verification Temporal specification languages Specification Mining/Inference Dr. Reger leads multiple EPSRC-funded research projects including SCorCH (Secure Code for Capability Hardware), CAPS (Collaborative Architectures for Proof Search), and QuTie (reasoning with Quantifiers and Theories). His work on the Vampire theorem prover and MarQ monitoring tool demonstrates his bridge between theoretical computer science and practical applications. Recent publications show strong focus on runtime verification, theorem proving, and program analysis with applications to security and performance monitoring. Notable awards: Highest Achiever of the Year Award for MSc studies Dr. Reger collaborates extensively with institutions including the University of Oxford, Arm, Amazon Web Services, and CERN (CMS Experiment). As Manchester lead on the SCorCH project, he develops formal analysis tools for security-aware hardware chips. His work on the VyPR framework enables developers to analyze Python program performance through temporal specification languages and monitoring algorithms.
Alp Bassa is a Professor of Mathematics at Boğaziçi University, affiliated with the Department of Mathematics. He holds a Ph.D. in Mathematics from Universität Duisburg-Essen (2007) and dual bachelor's degrees in Computer Engineering and Mathematics from Middle East Technical University (2004). His research focuses on Number Theory, Algebraic Geometry, and their applications in Cryptography and Finite Fields. Education: Ph.D. in Mathematics, Universität Duisburg-Essen, 2007 Bachelor of Science in Computer Engineering & Mathematics, Middle East Technical University, 2004 Research Interests: Professor Bassa investigates algebraic structures over finite fields, including Drinfeld modules, function fields, and their cryptographic applications. His work bridges Number Theory and Geometry, with contributions to coding theory and the construction of algebraic curves with optimal properties. Recent Projects: TÜBİTAK 2509: Curves over Finite Fields, Jacobian Varieties, and Abelian Varieties (2018–2020) BAP-10540: Curves over Finite Fields and Irreducible Polynomials (2015–2017) Teaching: Recent courses include foundational mathematics (Math 101, Math 102), advanced topics (Math 344, Math 525), and specialized courses in cryptography and algebraic geometry.
Dr. Hafizul Asad serves as a Lecturer in Dependability at City St George's, University of London, leveraging his PhD in Electrical Engineering (City University of London, 2016) and MS in Aerospace Engineering (University of Belgrade, 2008) to advance cybersecurity and formal verification research. His expertise bridges critical infrastructure protection and cyber-physical systems security, with significant contributions to IoT/IIoT security frameworks. His educational journey includes: PhD in Electrical Engineering, City, University of London (2012-2016) MS in Aerospace Engineering, University of Belgrade, Serbia (2007-2008) BSc in Electrical and Electronics Engineering, University of Engineering and Technology Peshawar, Pakistan (1999-2003) Asad's research centers on formal verification of hybrid systems and verifiable intrusion detection mechanisms for interconnected environments. He pioneers provably robust security architectures for IoT/IIoT systems, emphasizing mathematical verification to ensure system resilience against cyber threats. His work integrates diversity principles to create defense-in-depth strategies for critical infrastructure, with recent focus on wind turbine cyber-safety and industrial control system protection. Analysis of his 15 most recent publications (2014-2025) reveals an evolution from aerospace applications and analog circuit verification toward cutting-edge cybersecurity for cyber-physical systems. His 2023-2025 work demonstrates increasing specialization in IoT security and formal methods, while maintaining foundational contributions to diversity-based security architectures established in his 2015-2018 research. No scientific awards or prizes are documented in the provided materials, though he maintains professional standing as a British Computer Society member and Higher Education Academy Associate Fellow. Details regarding doctoral student supervision or specific research grants are not disclosed in the source text. His professional trajectory indicates significant project involvement, including the D3S security project at City University of London (2015-2018) and Rolls-Royce-funded Future Systems Simulator development at Cranfield University (2018-2019), though current laboratory affiliations remain unspecified.
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.
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
Krishnendu Chatterjee is a Professor at the Institute of Science and Technology Austria (IST Austria) , Department of Computer Science. His research spans formal verification, probabilistic systems, game theory, and evolutionary dynamics, with over 300 peer-reviewed publications in top venues such as DISC, AAAI, LICS, PNAS, Nature , and Journal of the ACM . His research focuses on developing theoretical foundations and practical algorithms for analyzing complex systems, including Markov decision processes, stochastic games, probabilistic programs, and evolutionary models. He has made significant contributions to topics such as reachability analysis, termination of probabilistic programs, synthesis of controllers, and evolutionary game dynamics. Chatterjee's work is highly interdisciplinary, bridging computer science, mathematics, and biology. He has collaborated extensively with leading researchers worldwide and has been involved in editorial roles and program committees for major conferences in formal methods and theoretical computer science.
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 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.
