Find Academic Supervisors

• Algebra
• Computational Complexity
• Theoretical Computer Science
• +3 more

Prof. Pawel M. Idziak is a distinguished academic at the Faculty of Mathematics and Computer Science, Jagiellonian University, where he holds a Professorship in the Department of Algorithmics. His primary research focuses on algebra, computational complexity, and theoretical computer science, with notable contributions to the study of algebraic structures, satisfiability problems, and modular circuits. Idziak has led and contributed to numerous grants, including managing the 'Numerical and Structural Invariants in Algebra, Logic and Constraint Satisfaction Problems' (2015–2022) and co-ordinating initiatives like 'Programmers of the Future 4.0'. His work bridges abstract algebra with computational challenges, addressing topics such as group theory, circuit satisfiability, and algorithmic complexity. His research interests span a broad spectrum of theoretical computer science and algebra, including the interplay between algebraic structures and computational problems. Idziak has advised over 20 PhD students, mentoring them in areas such as algorithm design, logic in computer science, and discrete mathematics. He has also contributed to foundational works like Generative Complexity in Algebra (2005) and co-authored influential papers in journals like SIAM Journal on Computing and Transactions of the American Mathematical Society . Idziak’s academic leadership is evident through his roles in institutional committees and his active participation in international conferences. His recent work (2024) on equation satisfiability in solvable groups highlights his ongoing contributions to advancing computational algebra and complexity theory.

• Constraint Satisfaction Problem
• Computational Complexity
• Universal Algebra
• +3 more

Dr. hab. Marcin Kozik is a Professor at the Department of Algorithmics within the Faculty of Mathematics and Computer Science at Jagiellonian University. His research focuses on Constraint Satisfaction Problems (CSP), Universal Algebra, and Computational Complexity. He has led multiple grants including 'Constraint Satisfaction Problems: Beyond the Finite Case' (2022–2026) and organized AAA 101 conference (2022). His work bridges algebraic methods with computational complexity, contributing to foundational theories in CSP dichotomy and robust algorithms. Research interests include algebraic approaches to CSP, complexity of finite algebras, and robust algorithms for near-unanimity CSPs. Recent publications emphasize quantum CSP strategies, unifying algebraic frameworks, and injective hardness conditions. He has received awards for his habilitation research (2011) and contributions in 2021. Grants Managed: Topological Correction Codes in Error-Resistant Quantum Computing (2022–2026) "Constraint Satisfaction Problems: Beyond the Finite Case" (Ministry of Science & Higher Education, 2022–2026) Key Contributions: Over 35 peer-reviewed articles, including foundational work on bounded width CSPs and absorption theory in universal algebra. Labs/Teams: Part of the Algorithmics Research Group, collaborating with Libor Barto, Andrei Bulatov, and others on CSP and algebraic complexity.

Håkon Robbestad GylterudView profile

Associate Professor

• Dependent Type Theory
• Homotopy Type Theory
• Logic in Computer Science
• +9 more

Håkon Robbestad Gylterud is an Associate Professor in the Department of Informatics at the University of Bergen, Norway. His academic work bridges mathematics and computer science, with a strong focus on logical foundations and formal systems. University: University of Bergen School: Faculty of Mathematics and Natural Sciences Department: Department of Informatics Position: Associate Professor His research centers on dependent type theory and homotopy type theory (HoTT), aiming to formalize mathematical reasoning and computational structures. He explores foundational concepts such as multisets, iterative sets, and data structures with symmetries within type-theoretic frameworks. His interests extend to category theory, algebra, topology, and the computer formalization of mathematics, emphasizing constructivity and rigorous logical modeling. The recent publications highlight a consistent trend in applying homotopy type theory to diverse mathematical structures—ranging from multisets and sets to planar graphs and category-theoretic constructions. These works demonstrate a deep engagement with univalent foundations and higher-dimensional reasoning, contributing to the theoretical robustness of type systems. No scientific awards are explicitly mentioned in the provided texts. Håkon advises research through collaborative publications, particularly with scholars like Jonathan Cubides and Daniel Gratzer. While no formal grants are listed, his sustained research output suggests active funding and academic support. He leads or contributes to research groups such as the Programming Theory group at UiB. He is involved in several research projects, including Algebraic Type Theory, Multisets and Sets in HoTT, Quoting Operations, and the Anti-Pattern Game. These initiatives reflect both serious theoretical inquiry and creative, interdisciplinary exploration.

Michal WalickiView profile

Associate Professor

• Mathematical Logic
• Philosophical Logic
• Graph Theory
• +13 more

Michal Walicki is an Associate Professor in the Department of Informatics at the University of Bergen, Norway. His research lies at the intersection of mathematical logic, theoretical computer science, and philosophy of logic. He specializes in graph-theoretic methods for analyzing logical paradoxes, paraconsistency, and the algebraic semantics of nondeterminism. His primary research interests include self-reference, semantic paradoxes, digraph kernels, paraconsistent logic, multialgebras, and bounded reasoning in epistemic logic. He has developed graph-based semantics for logical theories, where paradoxes correspond to graph cycles and consistent theories relate to digraph kernels. His recent work focuses on the Poison Game for infinite digraphs and a Logic of Sentential Operators (LSO) that handles unrestricted sentential quantification without explosion. His publications span journals such as the Journal of Philosophical Logic, Journal of Symbolic Logic, Synthese, and Discrete Mathematics. He has authored the textbook Introduction to Mathematical Logic and maintains comprehensive lecture notes for courses like INF-227. His work shows a strong trend in using combinatorial and algebraic structures to model logical and computational phenomena, especially in handling inconsistency and self-reference. Strongly complete axiomatizations of finite syntactic epistemic states Complete calculus for multialgebraic semantics of nondeterminism Graph Normal Form for first-order logic Paraconsistent resolution with local kernels Applications of digraph kernels to SAT solving Michal Walicki has supervised several PhD students, including Sjur Dyrkolbotn, Thomas Ågotnes, and Yngve Lamo. He has also received research funding for projects in logic and algebra, though specific grants are not detailed. He leads a research group focused on logical foundations of computation and collaborates with colleagues in logic, computer science, and philosophy. His work continues to explore the deep connections between logic, graphs, and algebraic structures.

Joost-Pieter KatoenView profile

Professor

• Probabilistic Programming
• Model Checking
• Formal Verification
• +4 more

Joost-Pieter Katoen is a full professor at RWTH Aachen University in Germany where he leads the Software Modeling and Verification (MOVES) group. Since 2013, he holds a distinguished professorship at RWTH Aachen University and is a member of the Academia Europaea. He also maintains a part-time association with the Formal Methods & Tools group at the University of Twente in the Netherlands. Professor Katoen's research primarily focuses on probabilistic programming, model checking, and formal verification. His work spans theoretical foundations of probabilistic systems, deductive verification techniques for probabilistic programs, and practical applications in software verification. He has made significant contributions to the development of algorithms for analyzing probabilistic models, including Markov chains and probabilistic automata. His research bridges theoretical computer science with practical verification challenges, particularly in the context of probabilistic systems. His recent publications reveal a strong focus on advancing probabilistic programming verification, with particular emphasis on generating functions, expected runtimes, and probabilistic bisimulation. The research trends show increasing sophistication in handling continuous distributions, parameter synthesis, and multi-objective verification problems. His work consistently appears in top-tier conferences including POPL, PLDI, SPLASH, and CAV. Scientific Awards and Recognition: Distinguished Professorship at RWTH Aachen University (since 2013) Member of Academia Europaea Professor Katoen has supervised numerous PhD students whose work spans various aspects of formal methods and probabilistic systems. His MOVES research group develops several verification tools including PROPHESY, PRINSYS, COMPASS, MRMC, and SMYLE. His editorial service includes membership on steering committees for major conferences such as CONCUR and ETAPS (where he serves as chair), and editorial boards for journals including STTT and PeerJ Computer Science.

Véronique BenzakenView profile

Professor

• Data-Centric Programming Languages
• Formal Verification of Data Management Systems
• XML/JSON Data Processing
• +3 more

Véronique Benzaken is a Full Professor at Université Paris-Saclay, affiliated with the Laboratoire de Méthodes Formelles (LRI) and INRIA Saclay's Toccata group. Her research focuses on Data-Centric Programming Languages , formal verification of data management systems, and type-safe XML/JSON processing. Key projects: ℂDuce XML-centric functional language, Datacert data certification initiative Collaboration with Oracle Labs on multi-lingual query interfaces using QIR Active in Coq formalization of SQL, Datalog, and data provenance Research interests include: Formal foundations for NoSQL/BigData languages Coq-based verification of database systems Type systems for data models Cloud computing data abstraction Her work bridges theory and practical implementation through collaborations with both academic and industrial partners.

Konstantinos MamourasView profile

Assistant Professor

• Programming Languages
• Formal Methods
• Runtime Verification
• +6 more

Konstantinos Mamouras is an Assistant Professor at the Department of Computer Science, Rice University. His research focuses on programming abstractions for data streams, runtime verification for cyber-physical systems, program semantics, and Kleene Algebra with Tests. Rice University, Houston, TX Department of Computer Science Research Interests : Design of programming abstractions for streaming data Runtime verification of cyber-physical systems Formal methods in program verification Kleene Algebra with Tests (equational theories) Efficient automata-based processing Quantitative monitoring frameworks Recent Scientific Contributions : 2025: Membership Testing for Semantic Regular Expressions (PLDI 2025) 2024: HybridSA GPU regex acceleration (OOPSLA 2024) 2024: Efficient regex with lookaround (POPL 2024) 2023: Bit Vector Automata for regex (OOPSLA 2023) 2021: Quantitative monitoring framework (RV 2021) Scientific Awards : 🏆 Distinguished Paper Award, PLDI 2024 🏆 Best Paper Award, EuroSys 2021 🏆 EATCS Best Theory Paper Award, FoSSaCS 2015 Advising : Mentored PhD student Lingkun Kong (2023) Advised MSc student Zhifu Wang (2022) Current advisees: Alexis Le Glaunec and Agnishom Chattopadhyay Teaching : Spring 2023: IoT Programming and Data Analysis (COMP 418/518) Fall 2022: Reasoning about Algorithms (COMP 382) Spring 2021: Reasoning about Software (COMP 403/503)

Mikołaj BojańczykView profile

Professor

• Automata Theory
• Logic in Computer Science
• Monadic Second-Order Logic
• +7 more

Mikołaj Bojańczyk is a Professor at the Institute of Informatics, Faculty of Mathematics, Informatics and Mechanics, University of Warsaw. He has been affiliated with the University of Warsaw since his undergraduate studies, with brief periods at institutions in Bordeaux and Paris (2004-2005). He received his PhD in 2004 under Igor Walukiewicz, completed his habilitation in 2008, and was promoted to full professor in 2014. Professor Bojańczyk's research lies at the intersection of theoretical computer science and mathematical logic, with a strong emphasis on automata theory. His work spans several interconnected domains: formal language theory, algebraic approaches to language recognition, monadic second-order logic and its extensions, polyregular functions, and the theory of atoms for handling infinite alphabets. He has made significant contributions to understanding the connections between logic and automata for various structures including words, trees, graphs, and data words. His research has particularly focused on characterizing logical definability through algebraic means, developing new automata models for complex structures, and exploring the boundaries of decidability for various logical formalisms. Analysis of his recent publications reveals a continued focus on polyregular functions, MSO transductions, and the theory of atoms. His work demonstrates a consistent pattern of connecting category-theoretic approaches with concrete automata models, often bridging abstract mathematical concepts with practical computational frameworks. A notable trend is his exploration of rank-based approaches in logic and graph theory, as well as deepening connections between algebraic structures and logical definability. Salomaa Prize (2024) PODS Test of Time Award (2016) PODS Best Paper (2013) Presburger Award (2010) Kuratowski Award (2007) Lipski Prize (2006) PODS Best Paper (2006) Ackermann Award (2005) ICALP Best Paper (2004) Professor Bojańczyk has successfully supervised numerous PhD students to completion, including Rafał Stefański (2023), Janusz Schmude (2022), and others dating back to Paweł Parys (2011). He currently supervises four ongoing PhD projects with Kacper Lewandowski, Katzper Michno, Antoni Puch, and Omid Yaghoubi. His grant portfolio demonstrates sustained research leadership, including the current NCN Maestro grant "Polynomial finite-state computation" (2023-2028), previous ERC Consolidator Grant "Lipa" (2016-2021), and ERC Starting Grant "Sosna" (2009-2014). He has also been active in academic service, serving on prestigious committees including the Gödel Prize Committee (2024-2026) and the Presburger Award Committee (2021-2023). Professor Bojańczyk has been instrumental in developing the "atoms" research program at the University of Warsaw, which has its own blog and book. This theoretical framework addresses computation with infinite alphabets through the lens of nominal sets and orbit-finite structures. He has also created educational resources including the "Automata Toolbox" lecture notes and the "Slajdomat" slide software for creating zooming presentations in Figma.

Hossein HojjatView profile

Assistant Professor

• Formal Methods
• Software Verification
• Hardware Verification
• +11 more

Hossein Hojjat is an Assistant Professor in the Department of Computer Science at the Rochester Institute of Technology (RIT), within the Golisano College of Computing and Information Sciences. He received his PhD in computer science from EPFL, Switzerland in 2013 and was a postdoctoral researcher at Cornell University before joining RIT. He is currently on leave from his academic position since 2019. Research Interests: His research focuses on formal methods for the analysis and verification of software and hardware systems. He works extensively on program verification, network verification (especially in software-defined networking), automated program repair, Horn clauses, interpolation techniques, and model checking. His work bridges theoretical foundations with practical tools and applications. Publication Trends: His recent publications (2012–2017) show a strong trend in applying formal methods to networked and distributed systems, particularly using NetKAT and Horn clause solvers. He has made significant contributions to ensuring consistency in network updates, synthesizing repairs, and analyzing timed and concurrent systems. His work integrates logic, programming languages, and systems. Scientific Service: Program Committee: FSEN 2015, FSEN 2017, TTCS 2017, VSTTE 2017, SEFM 2017, SBMF 2018, FSEN 2019 (co-chair), PLDI 2019 (AEC) Editorial Board: Information Processing Letters Advising and Grants: He has advised PhD student Ali Shokri and has received research funding through the SaTC: CORE: Small grant on federated network security. His academic advising and grant activities reflect his leadership in advancing formal techniques for secure and reliable systems. Labs and Teams: While no specific lab is mentioned, his collaborations with researchers at EPFL, Cornell, and in tool development (e.g., FLATA, ELDARICA) indicate active participation in formal methods research teams focused on verification toolkits and network programming.

Ohad KammarView profile

Academic

• Programming Language Theory
• Denotational Semantics
• Algebraic Effects
• +6 more

Ohad Kammar is a Reader at the School of Informatics, University of Edinburgh, where he is affiliated with the Laboratory for Foundations of Computer Science. His research bridges theoretical computer science with practical applications in programming languages, probabilistic computing, and conceptual biology. He holds a Royal Society University Research Fellowship focused on foundations for type-driven data science and is involved in multiple significant research projects including ARIA Safeguarded AI and differentiable probabilistic programming semantics. Dr. Kammar's research spans programming language theory with particular expertise in denotational semantics, algebraic effects, and probabilistic programming. His work explores how to formally model computational effects, create robust type systems, and develop mathematical foundations for probabilistic programming languages. He investigates connections between category theory, domain theory, and practical programming language design, with applications ranging from secure systems to Bayesian inference algorithms. His recent work shows increasing focus on type-driven approaches to data science and AI safety. Kammar's publication record demonstrates consistent high-impact contributions to top-tier programming language conferences (POPL, ICFP, LICS) with notable recognition including the POPL'19 Distinguished Paper Award and the 2025 ISCA Best Paper Award. His work shows a clear trajectory from foundational theory (algebraic effects, denotational semantics) toward practical applications in probabilistic programming and type-driven data science. Recent publications increasingly integrate concepts from category theory, domain theory, and statistical modeling to address challenges in programming language design for modern computing paradigms. 2025 ISCA Best Paper Award for 'Precise exceptions in relaxed architectures' POPL'19 Distinguished Paper Award for 'A Domain Theory for Statistical Probabilistic Programming' Dr. Kammar currently supervises UG4/MInf and MSc projects at the University of Edinburgh and is developing an undergraduate course on type-driven probabilistic modeling. His research is supported by prestigious grants including a Royal Society University Research Fellowship and collaborations with Facebook Research, the National Cyber Security Centre, and the Alan Turing Institute. His work often involves interdisciplinary teams spanning institutions including the University of Oxford, University of Cambridge, and KAIST. He is actively involved with the Laboratory for Foundations of Computer Science and the Bayes Centre at the University of Edinburgh. His recent projects include work with Ehud Lamm's Conceptual Biology Lab, demonstrating his interest in bridging computer science with biological concepts. Dr. Kammar is also known for his community service efforts to liberate academic papers from copyright restrictions, making important historical works in programming language theory more accessible to researchers.

Viktor KuncakView profile

Associate Professor

• Formal Verification
• Theorem Proving
• Program Synthesis
• +6 more

Viktor Kuncak is an Associate Professor at the École polytechnique fédérale de Lausanne (EPFL) in the School of Computer and Communication Sciences (IC) , affiliated with the Laboratory for Automated Reasoning and Analysis (LARA) . His work bridges programming languages, formal verification, and automated reasoning. Email: viktor.kuncak@epfl.ch Office: INR 318, EPFL, Lausanne, Switzerland Research Interests: Viktor specializes in formal verification , theorem proving , and program synthesis , focusing on languages, algorithms, and systems for automated reasoning. His research addresses verification of functional programs, constraint solving, and symbolic computation. Recent Publications Trends: His work includes mechanized HOL reasoning, algebraic array theories, interpolation in ortholattices, and symbolic automata complexity. Keywords span automated reasoning, formal methods, and functional programming. Scientific Awards: 2012: 5-year ERC grant (1.5M EUR) ACM SIGSOFT Distinguished Paper Award Invited talks at Lambda Days, Scala Days, and CACM Research Highlights Advising & Grants: Viktor has supervised 15+ PhD students and led a European COST network in automated reasoning. He served as Associate Editor for TOPLAS and co-chaired CAV, FMCAD, and VMCAI conferences. Labs & Teams: He leads LARA , which develops tools like Leon and Stainless for program verification and synthesis. The group focuses on scalable formal methods for reliable software.

Martin KreuzerView profile

Professor

• Computer Algebra
• Commutative Algebra
• Algebraic Geometry
• +3 more

Professor Martin Kreuzer holds the Chair of Mathematics with a focus on Symbolic Computation at the University of Passau's Faculty of Computer Science and Mathematics, a position he has occupied since 2007. His academic career centers on advanced mathematical research with significant applications in computer science and cryptography. Dr. Kreuzer's research focuses primarily on computer algebra, commutative algebra, and algebraic geometry, with special emphasis on algebraic cryptography. His work involves constructing new cryptosystems and analyzing the security of existing ones using algebraic methods. He investigates how mathematical equation systems can be used to formulate attacks on cryptosystems, particularly focusing on fault injection techniques where attackers provoke miscalculations in cryptographic hardware to deduce secret keys. This research contributes significantly to IT security and has grown increasingly important in recent years. His publication record shows a strong trend toward applied algebraic research, particularly in cryptographic applications and computational algebra. Recent work demonstrates expertise in zero-dimensional schemes, border basis theory, finite Z-algebras, and SAT solving techniques. The research spans theoretical mathematics while maintaining strong connections to practical security applications, especially in hardware security and post-quantum cryptography. Professor Kreuzer leads the DFG project 'Algebraic Error Attacks' (also referred to as 'Algebraic Fault Attacks'), which investigates the protection of cryptographic hardware against fault injections. This significant research initiative demonstrates his leadership in bridging theoretical mathematics with practical security challenges. His collaborative approach is evident through numerous co-authored publications with researchers including L. Robbiano, Le N. Long, F. Walsh, and others. These collaborations span multiple institutions and demonstrate his active role in the international mathematics and cryptography communities. Professor Kreuzer emphasizes the importance of interdisciplinary work, particularly with computer engineering, for the future design of secure cryptographic systems.

Harshit Jitendra MotwaniView profile

Research Fellow

• Computational Algebraic Geometry
• Formal Verification
• Tensors
• +5 more

Harshit Jitendra Motwani is a Postdoctoral Researcher at the Max Planck Institute for Software Systems (MPI-SWS) , Germany. Previously, he was a Postdoctoral Fellow at the Hong Kong University of Science and Technology (HKUST) (2023-2024), following doctoral research at Ghent University (2021-2023) and earlier engagements at HKUST, Ghent University, and the University of Bristol . Education : PhD in Mathematics: Algebra and Geometry from Ghent University (2021-2023), Thesis on Algebro-Geometric Algorithms for Program Synthesis; Integrated BSc and MSc in Mathematics and Computing from IIT Kharagpur (2015-2020). Research Focus : Integrates mathematics into computational domains, particularly Computational Algebraic Geometry , Formal Verification , and Tensors . His work spans program synthesis , tensor networks , conditional independence models , and control theory applications . Publications : Recent contributions include algorithmic advancements in formal methods (FM, AAAI, LAGOS), algebraic statistics (IMRN), and quantum computing (SIGMA). His research combines symbolic computation with practical software engineering challenges. Awards & Honors : IEEE Computer Society Larson Best Paper Award (2023) ACM SIGPLAN Distinguished Paper Award (2023) Young Researcher of the Heidelberg Laureate Forum (2023) INSPIRE Scholarship (2015-2020) Teaching : Guest Lecturer at HKUST, Teaching Assistant at RPTU Kaiserslautern-Landau and IIT Kharagpur. Mentored multiple bachelor's projects at Ghent University and IIT Kharagpur.

Rasmus Ejlers MøgelbergView profile

Professor

• Denotational semantics of programming languages
• type theory
• category theory
• +5 more

Rasmus Ejlers Møgelberg is a Professor at the IT University of Copenhagen, where he leads the Section for Theoretical Computer Science and coordinates the Programming, Logic and Semantics research group. His academic career includes prior postdoctoral positions at DISI (Universita di Genova) and LFCS (University of Edinburgh). His research spans denotational semantics of programming languages , type theory , category theory , guarded recursion , and domain theory , with applications in modeling computational effects and parametric polymorphism. Current work focuses on guarded type theory for reactive and probabilistic programming systems. Recent publications (2019-2025) demonstrate consistent innovation in guarded recursion frameworks, including denotational models for clocked type theory, guarded dependent types, and modal logics for reactive programming. Key trends involve bridging category theory with practical programming language features to handle recursion, concurrency, and probabilistic choice. He has supervised three PhD students to completion: Magnus Baunsgaard Kristensen (2022, Cubical Modal Type Theories), Christian Uldal Graulund (2021, Type Theories for Reactive Programming), and Marco Paviotti (2016, Denotational Semantics in Guarded Type Theory). Postdoctoral researchers include Maaike Zwart (current), Andrea Vezzosi, Niccolo Veltri, Bassel Mannaa, and Patrick Bahr (now ITU associate professor). His research is funded by the Independent Research Fund Denmark project "Algebraic Effects and Guarded Recursion" (2022-2025). As coordinator of the Programming, Logic and Semantics group, he directs theoretical research on programming language foundations, emphasizing denotational semantics and type systems for next-generation language design.

• Mathematics
• Computer Science
• Logic
• +3 more

Jose Gil-Ferez is an Assistant Professor in the Department of Mathematics at Schmid College of Science and Technology, Chapman University. He holds degrees from the University of Barcelona (BSc, MSc, PhD) and an additional PhD from the University of Cagliari. Education: University of Barcelona, Bachelor of Science University of Barcelona, Master of Science University of Barcelona, Ph.D. University of Cagliari, Ph.D. His research spans interdisciplinary areas in Mathematics and Computer Science, focusing on logic, algebraic structures, and historical mathematical analysis. Recent work includes exploring Euclidean geometry's foundational postulates and advancing balanced residuated partially ordered monoids' theoretical frameworks. His publications highlight trends in axiomatic systems , residuated lattices , and the history of mathematical proofs , reflecting collaborations with experts in algebraic methods and computer science. His office is located in the Keck Center for Science and Engineering, Room 366. Contact details: (714) 576-5725 | gilferez@chapman.edu .