جستجوی استاد راهنمای دانشگاهی

Hamed Nematiمشاهده پروفایل

استادیار

• Security of systems software
• Formal methods and program logics
• Interactive theorem proving
• +۲ مورد دیگر

Hamed Nemati is an Assistant Professor at the Division of Network and Systems Engineering under the School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology in Stockholm, Sweden. He was previously a Visiting Assistant Professor at Stanford University and a Research Group Leader at the Helmholtz Center for Information Security (CISPA) , where he also worked as a PostDoc and Research Fellow. Education : PhD in Computer Science from KTH Royal Institute of Technology Research Interests : Security of systems software, formal methods and program logics, interactive theorem proving, machine code analysis, applied machine learning Current Projects : Systematic verification of multi-language security protocols, hardware-software co-design for Spectre mitigation, capability-based access control models Scientific Awards : WASP (Wallenberg AI, Autonomous Systems and Software Program) faculty member Teaching Activities : Formal Methods in Security (Fall 2020-2023) at CISPA/Saarland University Digital Forensics and Incident Response (EP2780) (Fall 2024) at KTH

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

Karl Palmskog is a Lecturer at KTH Royal Institute of Technology in the Division of Theoretical Computer Science and the STEP research group. His work focuses on program verification and proof engineering, with particular emphasis on developing techniques and tools based on proof assistants for constructing functionally correct and secure software systems. Palmskog received his Ph.D. in Computer Science in 2014 from KTH, advised by Mads Dam, and his M.Sc. in Computer Science and Engineering from KTH in 2007. Prior to his current position, he was a postdoc at The University of Texas at Austin and University of Illinois at Urbana-Champaign. His research interests span programming languages, software engineering, and formal verification, with a particular focus on developing techniques and tools based on proof assistants. He is an avid user of the Coq proof assistant for both proving and programming, often complemented by OCaml, and also utilizes HOL4 and other ML family dialects. His work bridges theoretical foundations with practical applications, particularly in the domains of blockchain systems, distributed systems, and automotive software verification. Analysis of his recent publications reveals a strong focus on Coq-based verification, with significant contributions to proof engineering tools and methodologies. His work includes developing tools for regression proving, change impact analysis, mutation testing for Coq projects, and lemma name suggestion using deep learning. There's also a growing trend toward applying formal methods to real-world systems like blockchain protocols and automotive software. Palmskog has been involved in several research projects, including Coq-community Proof Engineering and Distributed Components. His past projects include Trustfull (SSF), Model-based Event Driven Scalable Programming for the Mobile Cloud (NSF), Highly Adaptable and Trustworthy Software (EU FP7), and 4WARD Future Internet (EU FP7). As an educator, Palmskog has served as examiner, course responsible, teacher, and assistant for various courses including Algorithms, Data Structures and Complexity; Degree Projects; Game Theory; Parallel and Distributed Computing; and Programming Paradigms. His work on Chip, a Coq formalization of change impact analysis, demonstrates his commitment to creating practical, certified tools that bridge formal methods with software engineering practice.

Peter Dybjerمشاهده پروفایل

استاد

• Intuitionistic Type Theory
• Categorical Type Theory
• Proof Assistants
• +۹ مورد دیگر

Peter Dybjer is a Professor of Computing Science at the Department of Computer Science and Engineering, Chalmers University of Technology in Sweden. He is a leading researcher in the field of type theory, with a focus on intuitionistic type theory, categorical semantics, and proof assistants. His work bridges foundational aspects of mathematics and computer science, emphasizing constructive methods and formal verification. Research Interests: Intuitionistic Type Theory and its categorical semantics Proof assistants and formal verification Inductive and inductive-recursive definitions Game semantics and normalization techniques Dependent type systems and their applications Homotopy Type Theory and univalent foundations Activities & Contributions: Editor of the Bulletin of Symbolic Logic Member of program committees for conferences like TYPES, FSCD, and MFPS Keynote speaker at events including the European Congress of Mathematics and the Hausdorff Research Institute's Summer School on Types, Sets, and Constructions Initiated and directed the Master's Program in Computer Science – Algorithms, Languages, and Logic at Chalmers Teaching & Outreach: Professor Dybjer has taught advanced courses at international summer schools, including: Inductive Definitions in Constructive Type Theory (TYPES Summer School, 2005) Dependent Types at Work (LerNet Summer School, Uruguay, 2008) Normalization by Evaluation (Midlands Graduate School, 2009 and 2015)

Lars-Henrik Erikssonمشاهده پروفایل

مدرس ارشد

• Formal Methods
• Logic in Computer Science
• Programming Language Theory
• +۷ مورد دیگر

Lars-Henrik Eriksson is a Senior Lecturer in the Department of Computer Science at Uppsala University, part of the Department of Information Technology. He holds a PhD and is recognized as an Excellent Teacher and educational mentor. He currently serves as the program director for the Master's program in Computer Science and has previously held leadership roles, including Head of the Department of Computer Science from 2004 to 2018. PhD in Computer Science Excellent Teacher Award Pedagogical Mentor at Uppsala University His research focuses on the applications of logic in computer science, particularly formal methods for software development. His work spans formal specification, verification, and synthesis, with strong emphasis on logic programming, interactive theorem proving, and logical frameworks. He has made significant contributions to the use of formal methods in safety-critical domains such as railway signaling. His current research includes modeling application domains within formal methods and formalizing concurrency theory using the Isabelle proof assistant. The recent publications reflect a sustained focus on modal logics for nominal transition systems, formal verification tools (e.g., GTO), and domain-specific applications of formal methods. These works demonstrate deep integration of theoretical logic and practical software engineering, especially in distributed and safety-critical systems. The recurring themes include concurrency, verification, and the use of domain models to enhance formal reasoning. Scientific Awards and Recognitions: Excellent Teacher Pedagogical Mentor Lars-Henrik Eriksson has advised numerous students through project supervision, thesis reviews, and course mentorship, though no formal list of advisees is provided. He has been involved in significant research management, including leading the department and directing a master’s program. He has also collaborated with industry, particularly in railway signaling, contributing to safety analysis and formal verification projects with Trafikverket and through companies he co-founded. He is a board member of Formal Methods Europe and served as program committee chair for the FME Symposium 2002 (part of FLoC’02). His work bridges academia and industry, especially in the application of formal methods to real-world engineering challenges.

Michael Minockمشاهده پروفایل

دانشیار

• Natural Language Interfaces
• Knowledge Representation
• Databases
• +۴ مورد دیگر

Michael Minock is an Associate Professor in Computing Science at Umeå University. His research focuses on the intersection of AI and relational databases, particularly in natural language interfaces, semantic tractability, and knowledge representation. He has led significant projects such as the VR grant (2015-04953) and EU STREP SpaceBook (2011–2014). Minock also co-founded C-Phrase Technologies AB and teaches courses on databases and large language models. B.S. in Computer Science (Honors), University of Michigan Ph.D. in Computer Science, UCLA His research explores the logical foundations of database query languages, emphasizing higher-order logic in natural language interfaces. Recent work integrates LLMs into database management systems. Key publication trends include query containment analysis, cooperative question answering, and context-aware navigation systems. Subfields span natural language processing, spatial databases, and semantic reasoning. Scientific Awards: Pell Grants Michigan Competitive Scholarship DARPA AASERT Award Minock's teaching includes courses on database management and LLM applications in IT. He actively contributes to open-access publications and maintains a strong interdisciplinary focus across AI, logic, and real-world database challenges.

• Automation
• Discrete Event Systems
• Supervisory Control
• +۳ مورد دیگر

Martin Fabian is a Professor at the Department of Electrical Engineering , Chalmers University . As Head of the Automation research group , he leads research initiatives in automation and discrete event systems. His research focuses on Supervisory control theory Formal verification Cyber-physical systems Robotics Manufacturing automation Recent publications (2024) highlight advancements in timed automata synthesis, smart contract verification, and disturbance-handling controller design. Earlier works (2023-2022) explore compositional algorithms, automated driving safety, and vehicle routing optimization.

Justin Pearsonمشاهده پروفایل

دانشیار

• Constraint Programming
• Combinatorial Optimisation
• Artificial Intelligence
• +۷ مورد دیگر

Justin Pearson is an Associate Professor at the Department of Information Technology; Division of Computing Science at Uppsala University . He is a member of the university's optimisation group and coordinates the IT department's mentor programme for new employees . Research Interests include Constraint Programming , Combinatorial Optimisation , Artificial Intelligence , Software Testing , and Complexity Theory . His work focuses on theoretical and practical aspects of constraint satisfaction, local search algorithms, and symmetry breaking in constraint programming. Teaching involves courses such as Algorithms and Data Structures II (1DL231) and Introduction to Machine Learning for Bachelor Students (1DL034), with a PhD-level course on Category Theory offered periodically based on demand. Scientific Contributions span publications in constraint programming for air traffic management, sensor networks, and industrial applications. Recent work includes parameterised treewidth in constraint models, time-series constraints, and symmetry breaking techniques. Students supervised include PhD candidates Frej Knutar Lewander (co-supervised with Pierre Flener), Yi Zhao (co-supervised with Di Yuan), and previously graduated students Gustav Björdal , María Andreína Francisco Rodríguez , and Joseph Scott .

• Type Theory
• Formal Methods
• Functional Programming
• +۳ مورد دیگر

Ana Bove is an Associate Professor (Docent) at Chalmers University of Technology and University of Gothenburg, affiliated with the Department of Computer Science and Engineering. She leads the Logic and Types unit in the Computing Science division since 2021. Her research focuses on type theory, formal methods, and programming languages, with contributions to dependent types, interactive theorem provers, and functional programming. Affiliations: Chalmers University, University of Gothenburg Roles: Head of Logic and Types unit, former Director of Studies (CSE), Project Manager (ForMath EU project) Her work emphasizes foundational aspects of programming languages and verified software. Notable projects include the ForMath EU initiative under Prof. Thierry Coquand. She has contributed to Agda and type systems, with over 28 publications in formal methods and theoretical computer science. Research interests include recursion models in type theory, partial functions, and alpha-structural induction. Her lab, the Logic and Types unit, explores advanced type systems and formal verification techniques.

Magnus Myreenمشاهده پروفایل

استاد

• Program Verification
• Interactive Theorem Proving
• Formal Methods
• +۸ مورد دیگر

Magnus Myreen is a Professor in the Department of Computer Science and Engineering at Chalmers University of Technology, where he leads research in program verification, interactive theorem proving, and verified software systems. He previously held a prestigious Royal Society University Research Fellowship at the University of Cambridge. Chalmers University of Technology — Professor (2023–present), Associate Professor (2015–2023) University of Cambridge — Royal Society Research Fellow (2012–2018) His research focuses on making formal verification practical and scalable, particularly through the CakeML project—a fully verified ML-style language with a bootstrapped compiler. He develops techniques in decompilation into logic, proof-producing synthesis, and verified runtimes for theorem provers like Milawa and HOL Light. His recent publications span top venues such as POPL, PLDI, ITP, and CAV, with a strong emphasis on verified compilation, compiler optimizations, and connecting verified components into larger systems (e.g., seL4 + CakeML). The work consistently targets real-world applicability and reduction of trusted computing bases. ACM SIGPLAN Most Influential POPL Paper Award (2014) BCS Distinguished Dissertation Competition Winner (2010) Amazon Research Award (2023) Royal Society University Research Fellowship Magnus has advised several PhD students including Oskar Abrahamsson, Alejandro Gomez, and Andreas Loow. His research has been funded by the Swedish Research Council and EPSRC. He is currently chair of the ITP steering committee and frequently serves on program committees for ITP, CPP, PLDI, and related conferences. He has led major collaborative efforts to connect verified systems, such as extending the seL4 microkernel verification down to machine code and proving the soundness of the Milawa theorem prover down to x86 machine code. He also works on verified synthesis of hardware and formal semantics of multiprocessor architectures.

Ulf Norellمشاهده پروفایل

پژوهشگر

• Interactive Theorem Proving
• Dependently Typed Programming
• Type Theory
• +۳ مورد دیگر

Ulf Norell is a Researcher at the Computing Science department of Chalmers University of Technology. He is an active member of both the Programming Logic and Functional Programming research groups, focusing on the intersection of theoretical type systems and practical programming language implementation. Dr. Norell completed his PhD at Chalmers University of Technology in 2007 with the dissertation "Towards a practical programming language based on dependent type theory," following a Licentiate thesis from Chalmers and Göteborg University in 2004 and a Master's degree from Chalmers in 2002. His educational background demonstrates a consistent focus on the theoretical foundations of programming languages. His research centers on making formal verification accessible through practical implementations of dependent type theory. Dr. Norell has made significant contributions to the Agda proof assistant, developing both the core system and the experimental AgdaLight platform. His work bridges advanced type theory with real-world programming challenges, particularly in the areas of parser implementation, mixfix operator handling, and generic programming techniques. The evolution of his publications shows a clear trajectory from foundational theoretical work toward increasingly practical applications of dependent types in programming. At Chalmers, Dr. Norell has taught Advanced Functional Programming (2008-2009) and Types for Programs and Proofs (2009), courses that directly reflect his research expertise. His teaching emphasizes the practical application of advanced type systems and formal methods. He maintains an active presence in the programming languages research community through conference presentations at venues including ICFP, TPHOLs, and MPC, where he demonstrates how dependent types can be used for interactive programming and formal verification in real-world contexts.

Moa Johanssonمشاهده پروفایل

دانشیار

• Artificial Intelligence
• Automated Reasoning
• Neuro-Symbolic Methods
• +۴ مورد دیگر

Moa Johansson is an Associate Professor (Docent) at the Department of Computer Science and Engineering, Chalmers University, Sweden. She serves as Co-Director of Chalmers' Area of Advance in Information and Communication Technology, driving interdisciplinary AI research. PhD in Automated Theorem Proving (University of Edinburgh, 2009) Postdoc at University of Verona (2009-2011) Her research spans neuro-symbolic AI methods , combining neural networks with symbolic reasoning for applications in mathematics, sports science, and political science. Current projects include: NeSSy (2023-): Neuro-symbolic synthesis via reinforcement learning Neurodynamic Programming (2023-): Agent communication learning Countering Bias in AI (2023-): NLP applications in social sciences Bias in Political Analysis (2020-2025): WASP-HS funded Recent publications focus on theory exploration , neuro-symbolic methods , and AI applications across disciplines. Scientific achievements include a VINNMER Marie Curie Fellowship and Best Paper Award at CICM 2014. Led TRACKS project course on sports digitalization Developed HipSpec automated inductive prover

• Automation Engineering
• Sustainable Production
• Robotics
• +۳ مورد دیگر

Bengt Lennartson is a Professor of Automation at Chalmers University of Technology and Head of the Department of Systems and Control Engineering. His research focuses on automation engineering, sustainable production, robotics, and energy optimization, with over 280 international publications. Collaborations include industry leaders like Volvo, Daimler, Kuka, and TetraPak. IEEE Fellow for contributions to automation systems Specializes in hybrid/discrete-event systems Develops energy optimization strategies for robotic production lines Recent work explores Plug-and-Produce systems , digital twin calibration , and stochastic energy optimization in robotics. His team integrates AI with formal methods for safety verification and develops open-source educational tools like biomedical exoskeletons. Scientific awards include IEEE Fellowship , with articles addressing energy-efficient robot trajectories, safety-aware multi-agent control, and formal verification of cyber-physical systems.