جست‌وجوی استاد و پژوهشگر

Mark van den Brandمشاهده پروفایل

استاد

• Software Engineering
• Digital Twin Engineering
• Model-Driven Engineering
• +۴ مورد دیگر

Mark van den Brand is a Full Professor of Software Engineering and Technology at Eindhoven University of Technology (TU/e), where he holds the chair in Software Engineering and serves as Scientific Director of the Digital Twin Lab (part of EAISI). He concurrently holds a Visiting Professorship at Royal Holloway University of London. His academic journey includes a PhD in Computer Science from Radboud University (1992), prior roles as part-time Associate Professor at Vrije Universiteit Amsterdam, and senior research positions at CWI. He also serves as Editor-in-Chief of the Journal on Software Engineering of Autonomous Systems (JSEAS) and editorial board member of Computer Languages, Systems and Structures . His research focuses on software engineering fundamentals, digital twins, model-driven engineering, safety-critical systems, and automotive software. Key contributions include work on domain-specific languages, model consistency, and safety assessment frameworks. He leads the Software Engineering and Technology cluster at TU/e and directs educational initiatives in the Department of Mathematics and Computer Science. Recent publications emphasize digital twin engineering, model management, and automotive systems safety. He collaborates internationally on projects like the C-ITS reference architecture and functional safety for autonomous driving. His work bridges academic research with industrial challenges through tools like SAMOS and COGENT, addressing scalability and consistency in large-scale systems. Current educational responsibilities include courses on programming, digital systems, and data science. He actively engages with industry through the TU/e innovation ecosystem, focusing on impactful research solutions for modern software engineering problems.

• Number Theory
• Algebraic Geometry
• Formalization of Mathematics
• +۳ مورد دیگر

Sander Dahmen is an Associate Professor in the Department of Mathematics at Vrije Universiteit Amsterdam. He is affiliated with the Faculty of Science and actively involved in academic research and teaching. His primary research interests include Number Theory, Algebraic Geometry, and the formalization of mathematical proofs. Dahmen has contributed to foundational work in areas such as Dedekind domains, class groups of global fields, elliptic curves, and Diophantine equations. He has led research projects including the 'Formalizing Diophantine algorithms' (2022–2026) and 'New Diophantine Directions' (2017–2022), focusing on algorithmic and computational aspects. He currently teaches courses such as 'Number Theory' and 'Project Computer Assisted Proofs'. His research has been supported by grants, including the NWO tenure-track grant (2014–2019). His publications span topics like formalizing mathematical structures, elliptic curve computations, and solving complex Diophantine equations. Dahmen also serves as an external member of the exam committee for Boswell-Bèta in Utrecht since 2021. His work bridges foundational mathematics with computational methods, emphasizing rigor through formal proof systems like Coq.

Paweł Garbaczمشاهده پروفایل

استادیار

• Formal Logic
• Ontology
• Philosophy of Computer Science
• +۳ مورد دیگر

Paweł Garbacz is an Assistant Professor at the Department of Computer Science Fundamentals within the Faculty of Philosophy at the Catholic University of Lublin. His work bridges formal logic, ontology, and their applications in computer science and philosophy. He has authored two books: Sentence Logic - One or Many and Logic and Artifacts . Research Focus: Formal logic, computational ontologies, philosophy of technical artifacts, and semantic interoperability. Publications: His recent work explores identity criteria, temporal logic, and the intersection of metaphysics with artificial intelligence. Collaborations: Active in interdisciplinary projects connecting philosophy with computer science, including contributions to the FOIS (Formal Ontology in Information Systems) conference series.

• Automated Reasoning
• Theorem Proving
• Machine Learning
• +۳ مورد دیگر

Professor Dr. rer. nat. Stephan Schulz is affiliated with DHBW Stuttgart (Faculty of Technology, Department of Computer Science). He leads student projects in automated reasoning and teaches courses like Formal Languages and Automata , Compiler Construction , and Logic and Foundations of Computer Science (2014-2025). His research focuses on integrating high-performance inference mechanisms and machine learning techniques for robust automated reasoning systems. He is the lead developer of E , a high-performance theorem prover for first-order and monomorphic higher-order logic with equality. E has dominated the CASC competition and is used for formal verification, automated deduction, and knowledge representation tasks. The system supports TFF/TH0 syntax and provides semi-readable proof objects with answer substitutions. Current PC roles: 15th IWIL (2024) co-chair, 25th LPAR (2024) member, 12th IJCAR (2024) member, Quantify-24 member, 9th PAAR (2024) member Major contributions: E theorem prover (versions 1.2-3.2), integration of SInE preprocessing, lambda-free higher-order logic support

Anne Baanenمشاهده پروفایل

مدرس

• Formal Verification
• Type Theory
• Logic
• +۴ مورد دیگر

Anne Baanen is a Lecturer in the Department of Computer Science at the Faculty of Science, Vrije Universiteit Amsterdam. They recently completed their PhD in theoretical computer science under the supervision of Jasmin Blanchette and Sander Dahmen as part of the Lean Forward project. Their current teaching responsibilities include coordinating the Logic and Modelling course and supervising projects in Computer Assisted Proofs. Their educational background includes double majors in Computing Science and Mathematics for both Bachelor's and Master's degrees at Utrecht University. During their time at Utrecht, they were active in student organizations, serving as chair of the programming committee WebCie and the LGBT+ organization TrotCie, while also contributing to the student newspaper de Vakidioot. Dr. Baanen's research operates at the intersection of computing science and mathematics, spanning intuitionistic logic, type theory, formal verification, and functional programming. Their work heavily involves the Lean theorem prover, focusing on formalizing advanced mathematical concepts like algebraic number theory, Dedekind domains, and class groups. They are particularly interested in the design of morphisms and substructures in dependent type theory, as evidenced by their presentations on bundling in type theory. Analysis of their publication record shows a consistent focus on formalizing mathematical structures using the Lean theorem prover, with particular emphasis on algebraic number theory and the design of effective type class systems. Their work bridges theoretical computer science and advanced mathematics, contributing to both the formal methods community and mathematical research. Dr. Baanen is also active in sustainable ecology, LGBT+ rights advocacy, and software freedom movements. Their teaching portfolio spans from Logical Verification to Grondslagen van de Wiskunde (Foundations of Mathematics), demonstrating both breadth and depth in computer science education. They have presented at numerous international conferences including CPP, ITP, IJCAR, and ICFP, establishing themselves as an emerging researcher in formal methods. Based in Amsterdam, they maintain an active research profile while contributing to the academic community through teaching and conference organization, including co-organizing the Formalization of Cohomology Theories workshop at BIRS in Banff, Canada.

Walter Guttmannمشاهده پروفایل

دانشیار

• Algebra of Computing
• Software Verification
• Formal Methods
• +۳ مورد دیگر

Walter Guttmann is an Associate Professor in the Computer Science and Software Engineering department at the University of Canterbury . He specializes in the Algebra of Computing , focusing on software correctness, formal verification, and semantic models for programming languages. Research Grants include JSPS Fellowships (2019, 2015) and DAAD Postdoc Fellowship (2010-2011) Conference Involvement spans RAMiCS (2026 co-chair), UTP (2019), and MPC (2015) His work bridges theoretical computer science with practical formal verification, particularly using Isabelle/HOL to mechanize proofs for graph algorithms like Prim's , Kruskal's , and Borůvka's . Recent publications formalize Stone relation algebras for weighted graph reasoning and develop modal algebras for concurrent dynamic logic. Scientific awards include: JSPS Invitation Fellowship (2019, 2015) DAAD Postdoc Fellowship (2010-2011) He has coordinated courses like COSC261 , COSC432 , and COSC470 , contributing to both undergraduate and postgraduate computer science education.

• Knowledge Representation
• Mathematical Knowledge Management
• Natural Language Processing
• +۵ مورد دیگر

Prof. Dr. Michael Kohlhase is a Professor in the Computer Science department at FAU Erlangen-Nürnberg and an Adjunct Associate Professor at Carnegie Mellon University . His work spans Computer Science and Formal Methods , focusing on Mathematical Knowledge Management (MKM), Knowledge Representation , and Natural Language Processing (NLP) in STEM domains. He leads the KWARC (Knowledge Adaptation and Reasoning for Content) research group, driving projects like OMDoc , sTeX , and MathHub . His research emphasizes modular logical foundations for mathematical knowledge and large-scale document corpora analysis, with applications in computer-supported education and semantic document systems . Collaborations include extended visits to institutions such as SRI International , University of Amsterdam , and University of Edinburgh . Key projects include developing scalable module systems for formal mathematics, theory graph models for knowledge integration, and mathematical search engines like MathWebSearch . His work bridges formal logic with practical software systems , ensuring interoperability across proof assistants , computer algebra systems , and educational tools .

Claudio Sacerdoti Coenمشاهده پروفایل

دانشیار

• Mathematical Knowledge Management
• Interactive Theorem Proving
• Logical Frameworks
• +۱۴ مورد دیگر

Claudio Sacerdoti Coen is an Associate Professor in Computer Science at the Department of Computer Science and Engineering , University of Bologna. His research focuses on Mathematical Knowledge Management , Interactive Theorem Proving , and their applications to functional programming languages and markup languages like XML and MathML. He has led the DAMA project for didactic applications of theorem provers. Employment: Associate Professor (2017–present), previously Lecturer (2007–2017) Education: Ph.D. in Computer Science (University of Bologna, 2004), Master’s in Computer Science (2000) Research Interests include: Integration of XML-based Mathematical Knowledge Management with Interactive Theorem Provers (e.g., Coq, Matita) Reduction strategies in the Calculus of (Co)Inductive Constructions Formal verification of algorithms and compilers Constructive analysis and formal topology User interface design for proof assistants Publications over the last decade highlight advancements in: Efficient substitution mechanisms for lambda calculi Formalization of mathematical theorems (e.g., Lebesgue’s Dominated Convergence Theorem) Development of proof assistant frameworks (Matita kernel, ELPI interpreter) Mathematical document structuring and search engine design

Benjamin Delawareمشاهده پروفایل

دانشیار

• Programming Languages
• Program Verification
• Formal Methods
• +۲ مورد دیگر

Benjamin Delaware is an active Associate Professor in the Department of Computer Science within Purdue University's College of Science. His research focuses on programming languages and formal verification, with significant contributions to relational verification, proof automation, and oblivious computation. His research interests span Programming Languages , Program Verification , Formal Methods , Relational Verification , and Proof Automation . Delaware develops techniques for verifying program correctness using type systems, automated reasoning, and language-based security approaches. His work bridges theoretical foundations with practical tools for secure and reliable software systems. Analysis of his recent publications shows strong trends in leveraging large language models for verification tasks (2025), advancing relational verification through E-graphs (2023-2025), and developing type-based approaches for security and privacy (2022-2024). His work consistently addresses fundamental challenges in program equivalence, test generation, and oblivious computation. Distinguished Reviewer (PLDI 2023) Delaware actively serves as committee member and session chair across major programming language conferences (POPL, PLDI, SPLASH). His grant activities focus on NSF-funded research in programming language theory and verification tools. He has mentored students through research papers and conference contributions, though specific advisees aren't listed in the source material. His work involves collaboration with research groups focused on formal methods and programming language design, particularly in developing verification frameworks like KestRel and Taypsi. Current projects explore LLM-assisted verification and policy-agnostic oblivious computation.

Toby Murrayمشاهده پروفایل

استاد

• Security
• Program Verification
• Formal Methods
• +۴ مورد دیگر

Professor Toby Murray is a faculty member at the University of Melbourne's School of Computing and Information Systems, where he serves as Director of the Defence Science Institute and Co-Lead of the Computer Science Research Group. He holds a D.Phil. in Computer Science from the University of Oxford (2011) and previously worked at NICTA/Data61 and UNSW. His research focuses on security verification , neural network robustness , and software security , with projects including Verisimilar (verified secure ML), EDEFuzz (API vulnerability detection), and COVERN (concurrent program security). His work bridges formal methods with practical cybersecurity challenges, particularly in adversarial environments. Publication trends show consistent contributions in formal verification (35% of recent papers), security testing (30%), concurrency models (20%), and neural network security (15%), with evolving focus toward AI safety and web API vulnerabilities. Distinguished Paper Award at ICSE 2024 He leads a research group with 7+ PhD students and postdocs, focusing on cybersecurity assurance and collaborative fuzzing techniques. His team develops tools like Legion (test case generation) and Underflow (vulnerability detection).

André Platzerمشاهده پروفایل

استاد

• Logic in Computer Science
• Cyber-Physical Systems
• Programming Languages
• +۴ مورد دیگر

André Platzer is a Professor at Karlsruhe Institute of Technology (KIT), holding the Alexander von Humboldt Professorship for Logic of Autonomous Dynamical Systems. He previously served as an Associate Professor and later as a full professor at Carnegie Mellon University (CMU), where he founded the Logical Systems Lab. His research focuses on the logical foundations of cyber-physical systems (CPS), aiming to ensure safety-critical computer control of physical processes through formal verification and programming language design. Education Ph.D. in Computer Science, University of Oldenburg, Germany Platzer's research interests center on logic-based verification of cyber-physical systems, hybrid systems, and programming languages. His work develops differential dynamic logic and tools like KeYmaera X to mathematically prove safety in autonomous systems, impacting areas such as transportation and medical robotics. Publication Trends : His recent work emphasizes invariant generation, formal verification of reinforcement learning, and quantifier elimination in Isabelle/HOL, aligning with his focus on mathematical guarantees for CPS safety. Awards ACM Doctoral Dissertation Honorable Mention NSF CAREER Award Popular Science Brilliant 10 Young Scientist IEEE Intelligent Systems AI's 10 to Watch Students : His advisees include award-winning researchers like Yong Kiam Tan (CMU Distinguished Dissertation Award), Katherine Kosaian (Bill McCune PhD Award), and Sarah Loos (CMU Honorable Mention). Labs : Founded the Logical Systems Lab at CMU and leads reliability research at KIT's Institute for the Reliability of Autonomous Dynamical Systems.

Enrico Tassiمشاهده پروفایل

پژوهشگر

• Interactive Theorem Proving
• Formal Verification
• Type Theory
• +۵ مورد دیگر

Enrico Tassi is a researcher at Inria, France, affiliated with the STAMP team. His work focuses on the technology of formal proofs, particularly type theory, interactive theorem proving, and its application to formalizing mathematics. He is a key contributor to the development of tools like Coq-Elpi , Hierarchy-Builder , and the small scale reflection Coq extension. His research spans proof assistant architecture, software design, and formal verification, with a strong emphasis on free software principles. Enrico completed his Ph.D. at the University of Bologna in 2008, where he designed the Matita interactive theorem prover. He contributed to the formalization of the Odd Order Theorem and the Paral-ITP project, aiming to scale Coq for large mathematical libraries. His software projects include Elpi , a meta-language for proof assistants, and past contributions to Debian as a developer (2006–2016), focusing on integrating the Lua language into Debian systems. His publications highlight innovations in unification algorithms, tactical design, and proof structuring techniques. Articles address challenges in bi-directional type inference, pattern-based proof command focusing, and nonuniform coercion implementations. His work on small-scale reflection and Hierarchy-Builder demonstrates expertise in algebraic hierarchies and formal library management. Current efforts target enhancing OCaml-based systems through Elpi's high-level programming capabilities. Key Collaborations : Mathematical Components team (INRIA), D.A.M.A. Project Major Tools : Coq-Elpi, Hierarchy-Builder, Matita Formalization Efforts : Ordered Uniformities, Odd Order Theorem, Finite Group Theory

Elsa L Gunterمشاهده پروفایل

استاد پژوهشی

• Formal Methods
• Programming Languages
• Software Engineering
• +۷ مورد دیگر

Elsa L Gunter is a Research Professor and Senior Lecturer at the University of Illinois at Urbana-Champaign's Department of Computer Science. Her academic background includes a Ph.D. in Mathematics from the University of Wisconsin, Madison. She leads research in formal methods, programming languages, and human-computer systems. Research Interests: Her work spans formal verification, programming language semantics, automated theorem proving, and security. She develops tools for compiler optimization verification, human-automation system safety, and concurrent program analysis. Key projects include the VeriF-OPT framework for parallel program transformations and Tutela for human-computer system protection analysis. Publications Focus: Her recent research emphasizes compiler verification, concurrency models, and human-system interaction. Work includes symbolic analysis for CSP, dependently-typed session systems, and robustness verification for safety-critical interfaces. Awards: Most Influential 10 Year Paper award at Requirements Engineering (RE 2010) EASST Best Software Science Paper at ETAPS 2001 Best Paper award at Fourth International Conference on Requirements Engineering (2000) Funding and Labs: Secured NSF grants for projects on parallel program verification ($450K) and human task analysis ($500K). Leads the Formal Methods and Verification Lab, collaborating with NASA on NextGen aviation systems. Student Advising: Mentored 7 PhD graduates and 12+ Master's students. Current PhD candidates work on secure distributed programming (Dennis Griffith) and formal methods for concurrent systems (Liyi Li, Susannah Johnson).

Tobias Nipkowمشاهده پروفایل

استاد

• Term Rewriting
• Theorem Proving
• Formal Methods
• +۳ مورد دیگر

Tobias Nipkow is a full Professor at the Faculty of Informatics, Technical University of Munich (TUM), Germany, where he leads the Theorem Proving Group and maintains active academic duties as evidenced by ongoing conference commitments through 2026. His office is located at Boltzmannstr. 3, 85748 Garching, with contact email nipkow@in.tum.de and office hours held Wednesdays 11:00-12:00 during semester periods. Nipkow serves on CPP Steering Committees (2015-2026) and Program Committees (2018, 2023), reflecting sustained leadership in programming language research. His seminal work spans term rewriting systems and theorem proving, established through the authoritative text Term Rewriting and All That (Cambridge University Press, 1998). Current research emphasizes formal verification using Isabelle/HOL, with extensions into verified functional algorithms ( Functional Algorithms, Verified! ), concrete semantics education, and probabilistic program verification. This integrates theoretical computer science with practical proof assistant applications, focusing on termination, confluence, and unification in rewriting systems. Recent publications demonstrate a clear trajectory toward educational applications of formal methods and foundational data structure verification. The 2021 CPP invited talk explores proof assistants for teaching algorithms, while the 2020 CPP proof pearl formalizes Braun trees using Isabelle. Earlier work like the 2015 ESOP paper on verified probability density compilers shows consistent themes of mechanized semantics and verification. These outputs highlight his dedication to bridging theoretical concepts with classroom and industrial practice. Nipkow directs TUM's Theorem Proving Group, the core development team for the Isabelle interactive proof assistant. The group maintains the Archive of Formal Proofs (isa-afp.org), a major repository of formalized mathematics, and organizes annual Isabelle Workshops. Their work underpins verification projects across academia and industry, with direct influence on ITP and CPP conference series through leadership roles and tutorial development.

• Interactive Theorem Proving
• Formalization of Mathematics
• Proof by Reflection
• +۳ مورد دیگر

Kazuhiko Sakaguchi is a Researcher affiliated with CNRS (French National Centre for Scientific Research), École Normale Supérieure de Lyon (ENS Lyon) , and Université Claude Bernard Lyon 1 , working at the Laboratoire de l'Informatique du Parallélisme (LIP, UMR 5668) . His primary research focuses on foundational aspects of programming languages and formal verification. Research Interests: Sakaguchi specializes in interactive theorem proving (particularly using Coq), formalization of mathematics , and proof by reflection . His work bridges theoretical computer science and practical tool development, with applications in algorithm verification, algebraic hierarchies, and dependent type systems. Publication Trends: His recent articles emphasize formal verification of algorithms (e.g., mergesort correctness), design patterns for mathematical structures in proof assistants, and program extraction techniques. A consistent theme is enhancing productivity in theorem proving through reusable abstractions and automated tactics.