Hans Tompits is an Associate Professor in the Department of Knowledge-Based Systems at Technische Universität Wien (Vienna University of Technology). His research focuses on computational logic, declarative logic programming, and formal methods, with a particular emphasis on Answer-Set Programming (ASP). He coordinates the Master's program in Logic and Computation and leads projects in areas such as formal methods for optimization, fault-tolerant autonomous systems, and algorithmic composition. His work bridges theoretical advancements with practical applications, including tools like SeaLion (an ASP IDE with debugging support) and dlvhex (an ASP-based semantic web reasoner). He has contributed to foundational topics like program equivalence, debugging techniques, and integration of ASP with external systems. His recent projects address challenges in autonomous vehicle architectures, music composition algorithms, and safety-critical system design. Tompits has published extensively on topics ranging from nonmonotonic reasoning and modal logics to the development of declarative programming tools. His interdisciplinary approach spans computer science, mathematics, and AI, with applications in both academic and industrial contexts.
Xavier Parent is a Researcher in the Department of Theory and Logic at Technische Universität Wien (TU Wien). His work focuses on deontic logic, normative reasoning, and proof theory, with applications to AI and legal systems. He leads the LoDEx project (2024–2026) and previously contributed to the Lisa Meitner grant (2021–2024) and TICAMORE project (2017–2022). His research emphasizes formal verification of normative systems using higher-order logic (HOL) and explores topics like conditional obligations, dyadic deontic structures, and automated reasoning. Key projects include: LoDEx: Developing logical methods for deontic explanations Lisa Meitner Grant: Investigating permissive norms and regulative norms TICAMORE: Embedding dyadic deontic logic in HOL His research interests span: Formal semantics of normative systems Automated theorem proving for deontic logics Interactions between betterness orderings and obligations Publications highlight contributions to journals like Journal of Philosophical Logic and Journal of Applied Non-Classical Logics , with conference presentations at DEON, PRIMA, and Dagstuhl Seminars. He advises students like David Pichler on extensionality in normative systems.
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.
Franz Wotawa is a Professor of Software Engineering at Graz University of Technology. He holds a M.Sc. (1994) and PhD (1996) from Vienna University of Technology. He has served as head of the Institute for Software Technology from 2003–2009 and since 2020. His research focuses on model-based reasoning, software testing, autonomous systems, and diagnosis, with over 390 peer-reviewed publications. He founded Softnet Austria (2006) to bridge research and industry. He leads the Christian Doppler Laboratory for Quality Assurance Methodologies for Autonomous Cyber-Physical Systems since 2017 and has supervised 90+ master and 36+ PhD students. His awards include the 2016 Lifetime Achievement Award from the International Diagnosis Community. He is a member of Academia Europaea, IEEE, and AAAI. **Education**: M.Sc. in Computer Science, Vienna University of Technology, 1994 PhD, Vienna University of Technology, 1996 **Research Interests**: Model-based reasoning, qualitative reasoning, theorem proving, mobile robotics, verification/validation, software testing/debugging, AI, and autonomous systems. **Notable Projects**: A-IQ Ready (2022–2026): Quantum sensing for autonomous systems. ALFA (2024–2027): AI for smart diagnosis in building automation. Bilateral AI (2024–2029): Combining symbolic and sub-symbolic AI. VARCOS (2025–2028): Vehicle-road cooperative systems for autonomous driving. **Awards & Memberships**: Lifetime Achievement Award (2016, International Diagnosis Community) Senior Member, AAAI Member of Academia Europaea, IEEE, ACM, and Austrian Computer Society **Labs/Teams**: Christian Doppler Laboratory for Quality Assurance Methodologies (since 2017). Active in Cluster of Excellence “Bilateral AI” at TU Graz.
Javier Esparza is a Professor and Chair of Foundations of Software Reliability and Theoretical Computer Science at the Technical University of Munich (TUM), Germany. He has held academic positions at several prestigious institutions including the University of Stuttgart, University of Edinburgh, and Technische Universität München since 1990. His work focuses on theoretical computer science with applications in software verification and formal methods. His educational background includes: M.S. in (Theoretical) Physics from the University of Zaragoza (Spain, 1987) Ph.D. in Computer Science from the University of Zaragoza (Spain, 1990) Habilitation in Computer Science from the University of Hildesheim (Germany, 1994) Professor Esparza's research interests span multiple areas of theoretical computer science and formal methods. He has made significant contributions to the fields of software verification, model checking, and Petri nets. His work on algorithms for the design and verification of reactive and distributed systems has been particularly influential. He has developed theoretical foundations and practical tools for analyzing systems with infinitely many states, pushing the boundaries of what can be formally verified. His research on formal models for distributed systems, particularly Petri nets and process algebras, has provided new insights into concurrency theory. Additionally, his work on the analysis of probabilistic systems and applications of linear and constraint programming to verification problems has opened new avenues for research. His recent publications demonstrate a continued focus on fundamental problems in verification and theoretical computer science, with particular emphasis on population protocols, model checking techniques, and theoretical foundations of distributed computing. His work bridges the gap between theoretical insights and practical applications in software reliability. His scientific achievements have been recognized with several prestigious awards: Doctor honoris causa in Informatics, Masaryk University (2009) Dissertation prize, University of Zaragoza (1990) TeachInf Award for best Bachelor course at TU München (2009) TeachInf Award for best Master course at TU München (2010) Diploma for excellent Teaching, TU München (2011) Member of Academia Europaea (2011) Professor Esparza has successfully advised numerous PhD students who have gone on to make their own significant contributions to computer science. His research has been consistently supported by competitive grants from major funding bodies including the German Research Council (DFG), the British Engineering and Physical Sciences Research Council, and the European Union. His research projects have often involved international collaborations, reflecting the global recognition of his work. He leads a vibrant research group at TUM focused on theoretical computer science and verification. The group has developed several influential software tools including Rabinizer, Peregrine, Owl, and Strix, which are widely used in both academia and industry for verification tasks. His group maintains strong collaborations with research institutions worldwide, particularly in Europe.
Prof. Sagiv Shmuel is a Full Professor at Tel-Aviv University's Department of Computer Science. He has held various academic roles, including Associate Professor (2004–2005), Senior Lecturer (2000–2004), and visiting positions at institutions such as the University of Chicago and University of Copenhagen. His research focuses on software verification, shape analysis, smart contracts, and programming languages. Education: Ph.D. in Computer Science, Technion (1986–1990) B.A. in Computer Science, Technion (1982–1985), cum laude Research Interests: His work addresses challenges in static analysis, formal verification, and program analysis. Notable areas include invariant inference, smart contract security, and parametric shape analysis. These contributions have led to practical tools like Ivy and the foundation of Certora, a company specializing in smart contract verification. Awards: ACM Fellow (2016) Friedrich Wilhelm Bessel Research Award (2002) Microsoft Outstanding Collaborator Award (2016) Grants & Leadership: Principal Investigator (PI) of a Senior ERC Grant (1.57M Euros) for software composition verification Editor of Foundations and Trends in Programming Languages Chair of program committees for POPL, SAS, and other leading conferences His research has been applied to real-world systems, such as improving the Java concurrent library and ensuring kernel extension security in Linux.
Martin Riener is a Senior Lecturer at the Department of Theory and Logic, Faculty of Informatics, TU Wien. His research focuses on automated theorem proving, higher-order logic, and formal methods. He contributes to the GAPT framework for proof theory and collaborates on the Vampire theorem prover. He has worked on projects like CERESω cut-elimination and TLAPM for TLA+. Education: PhD (2017) and MSc (2011) in Computer Science from TU Wien. Research projects include an Austrian Science Fund (FWF) project (2010–2012) on proof-theoretic applications of CERES. Teaching includes courses on programming fundamentals, digital systems, and formal modeling. He is involved in outreach activities explaining computer science concepts through unplugged activities for diverse age groups. Software contributions include GAPT, Vampire, and TLAPS. Contactable via three email addresses and ORCID: 0000-0001-8836-7808 .
Wolfgang Windsteiger is an Associate Professor at the Research Institute for Symbolic Computation (RISC) of Johannes Kepler University (JKU), Linz, Austria. His primary research focuses on automated theorem proving, computer algebra systems, and symbolic computation, particularly within the Theorema project. He leads the redesign and implementation of Theorema 2.0, an open-source system for mathematical theory exploration. Windsteiger is also active in integrating computational tools into mathematics education, co-authoring textbooks on algorithmic methods for university students. His work spans formal methods, mathematical software development, and educational technology. Positions: Associate Professor at RISC/JKU, Trustee of Calculemus, Conference Chair of multiple events including Calculemus'2007 and MKM'2007. Contributions: Developer of Theorema 2.0, co-author of Springer's 'Algorithmische Methoden' series, and creator of educational software tools for mathematics. Research Interests: Theorema system development, automated reasoning, formal methods in economics, and computational pedagogy. He actively promotes the use of theorem provers in university and school-level mathematics education.
Christine Paulin-Mohring is a Full Professor at Université Paris-Saclay's Faculty of Science since 1997. She previously held a secondment at INRIA Futurs/Saclay Île-de-France (2006-2008), was a CNRS Researcher at ENS Lyon (1989-1997), and an assistant professor at ENS Paris (1985-1989). She earned her PhD in 1989 from Université Paris 7 under Gérard Huet's supervision at INRIA Rocquencourt and ENS Paris. Her research focuses on Program verification Type theory Interactive theorem proving Formal methods Coq proof assistant Randomized algorithms She has developed the ALEA Coq library for randomized programs and led the ProVal research group until 2011. Her award highlights include ACM Software System Award (2013) Doctor Honoris Causa from University of Gothenburg (2011) Prix Michel Monpetit (2015) Academia Europaea membership (2014) She has advised 15 PhD students and coordinated major projects like DigiCosme Labex (2007-2011). Her administrative roles include Dean of the Faculty of Science (2016-2021) and leadership in doctoral schools.
René Thiemann is an Associate Professor in the Department of Computer Science at the University of Innsbruck, Austria, where he is a key member of the Computational Logic Group. His work bridges theoretical computer science and practical formal verification, with a strong emphasis on automated reasoning and program correctness. Research Interests: Program Verification using interactive theorem proving (Isabelle/HOL) Termination and complexity analysis of programs Term rewriting systems and dependency pairs SAT/SMT solving and decision procedures Formalization of algebraic algorithms (LLL, Smith normal form, algebraic numbers) Development of the Certification Problem Format (CPF) and the CeTA tool His recent publications (2017–2025) reflect a consistent focus on formalizing advanced algorithms in Isabelle/HOL, especially those related to termination, complexity, and algebraic computation. These works are published in top venues like CPP, FSCD, LICS, and ITP, demonstrating rigorous, machine-checked proofs. His research often centers on verifying tools like AProVE and developing foundational libraries for number theory and rewriting. Scientific Projects: ARI : Automation of Rewriting Infrastructure (Task Leader, since 2022) Certifying Termination and Complexity Proofs : Project Leader (2014–2021) Constrained Rewriting and SMT : Task Leader (2012–2015) Improving Certifiers for Termination Proofs : Project Leader (2010–2014) Teaching Activities: Lecture and Proseminar: Program Verification (SS 2023–2025) Lecture: Constraint Solving (SS 2024–2025) Lecture and Proseminar: Functional Programming (WS 2021–2025) Lecture: Advanced Functional Programming (WS 2024/25) Lecture: Interactive Theorem Proving in Isabelle/HOL (SS 2022–2024) Lecture: Decision Procedures (SS 2021) He has supervised no listed students in the provided data but actively contributes to collaborative research. His email is rene.thiemann@uibk.ac.at.
Roles & Affiliations: Bruno Buchberger is a Research Professor at the Research Institute for Symbolic Computation (RISC) and the University of Linz (Johannes Kepler University), Austria. He is also the Honorary Professor at the Technical University of Vienna and the founder of the Softwarepark Hagenberg. He has held visiting positions at institutions worldwide, including Kyoto University, Texas A&M, and the University of Timisoara. Head of Softwarepark Hagenberg Member of Academia Europaea, London Corresponding Member of the Bavarian Academy of Science Education: PhD in Mathematics (1966), University of Innsbruck, under Wolfgang Gröbner Matura Exam (1960), Realgymnasium Angerzellgasse, Innsbruck Research Focus: Buchberger is renowned for inventing the Gröbner Bases theory and developing the Theorema system for natural-style mathematical reasoning. His work bridges symbolic computation, automated theorem proving, and algorithm synthesis. Key areas include: Algorithmic Mathematics Computer Algebra Systems Formal Methods Mathematical Theory Exploration Article Trends: Recent works explore automated theorem proving, AI integration in mathematics education (e.g., ChatGPT analysis), and algorithmic methods for special functions (e.g., Ramanujan-Sato series). His contributions emphasize interdisciplinary applications in software science and computational mathematics. Awards: ACM Kanellakis Award (2007) Austrian Cross of Honors (2003) Austrian of the Year (2010) Multiple honorary doctorates (Bath, Nijmegen, Timisoara) Grants & Teams: Led the Gröbner Bases Special Semester 2006 at RICAM. Involved in the SFB13 consortium for Scientific Computing. Collaborated with the Japanese Society for Symbolic Computation and the Radon Institute. Labs & Initiatives: Founded RISC (1987) and Softwarepark Hagenberg (1991), catalyzing Austria’s tech ecosystem. Key projects include the Theorema system and educational programs like the Informatics Master’s program in Hagenberg.
Florian Sextl is a Research Fellow and university assistant at the Formal Methods in Systems Engineering research unit at TU Wien, where he conducts research on program verification and formal foundations of programming languages. His work focuses on memory safety fundamentals, particularly through separation logic-based methods and the Rust programming language. Current projects explore biabduction techniques for ensuring memory safety across Rust-C foreign function interfaces and compositional shape analysis. Sextl teaches Program Analysis courses and has supervised research on join operators for bi-abductive analysis of low-level code. He maintains expertise in interactive theorem proving with Isabelle/HOL and Rocq.
Stefan Hetzl is an Associate Professor at Vienna University of Technology (TU Wien), affiliated with the School of Informatics and the Institute of Computer Science. His research focuses on computational logic, proof theory, and formal languages, with a particular emphasis on automated and interactive theorem proving. He contributes to the development of the GAPT system for proof analysis and participates in projects like the Automated Analysis of Mathematical Proofs funded by the Austrian Science Fund (FWF). Interactive Theorem Proving Automated Theorem Proving Proof Theory Theory of Formal Languages Hetzl has supervised multiple academic theses, including Diploma Theses on topics such as open induction, finite languages, and cyclic superposition. His publications span areas like cut-elimination, Herbrand sequents, and higher-order logic, reflecting a deep engagement with structural invariance and algorithmic transformations in formal proofs. While no explicit awards are listed, his work contributes significantly to the theoretical foundations of computer science and mathematical logic.
Tobias Nipkow is a Professor for Logic and Verification at the Department of Informatics, Technical University of Munich (since 2011), previously serving as Professor for Theory of Programming (1992-2011). His career spans academic roles at The University of Manchester, MIT, and University of Cambridge, including positions as Lecturer, Research Associate, and Advanced SERC Fellow. Research Interests focus on foundational aspects of computer science, particularly Formal verification of algorithms and systems Interactive theorem proving Term rewriting systems Semantics of programming languages Development of proof assistants Automated reasoning techniques Notable Publication Trends include extensive contributions to Isabelle/HOL formalization, verification of programming languages, and critical advancements in term rewriting and automated deduction. His work bridges theoretical foundations with practical verification tools. Scientific Awards Herbrand Award for Distinguished Contributions to Automated Reasoning (2021) Editorial Leadership includes tenure as Editor-in-Chief of the Journal of Automated Reasoning (2007-2020) and co-founding editor roles for ACM Transactions in Computational Logic and Logical Methods in Computer Science .
