Gerardo Schneider

My research focus on formal specification and analysis of contracts, formalization of privacy policies, model checking, verification of real-time and polygonal hybrid systems, verification of embedded systems (in particular smart java cards), semantics, logics for computer science, security.

faculty Division Head


Wolfgang Ahrendt

My research focus on deductive software verification on Java programs, combined static and runtime verification, smart contracts verification, object-oriented program verification.

faculty


Magnus Myreen

program verification, interactive theorem proving and, particularly, the challenges of making interactive proofs more automatic / scale to real code. My most recent work has focused on CakeML, which is an ML-style language with a formal semantics and a growing ecosystem of proofs and tools that support construction of verified applications. CakeML compiler is the first verified compiler to have been bootstrapped.

faculty


Moa Johansson

learning and exploration in automated theorem proving, automated reasoning about recursive programs, reasoning for program analysis, automated discovery of inductive lemmas.

faculty


Nir Piterman

My research interests include formal verification and automata theory. I have worked (and still am) on model checking of various types of systems, different aspects of temporal logic, as well as synthesis and game solving. I am also working on applications of formal methods to biological modeling.

faculty


Laura Kovács

My research is on formal software analysis and verification. More specifically, I am interested in designing new methods for computer-aided verification by combining: automated theorem proving, automated assertion generation, symbolic computation.

faculty


Sandro Stucki

In my research, I like to explore the many aspects of programming languages. I'm particularly interested in type systems and theory, the semantics and implementation of domain-specific languages, as well as formal methods for scientific modeling. Until recently, I spent my time pondering the type safety of Scala and related type systems. These days, I’m busy applying formal methods and type theory to problems in privacy and security, and hacking type soundness proofs in Agda. I'm interested in the design of domain-specific languages for modeling probabilistic and stochastic systems, especially biochemical systems. I have also written a GNU/Emacs mode for Kappa, a modeling language for systems biology.

PostDoc


...
Yehia Abd Alrahman

My own sphere of special interest in the field of Computer Science is comprised by the challenge of supporting the development of high-quality, correct-by-construction software and systems, featuring predictability, adaptivity, efficiency, re-usability, maintainability and modularity that are key issues in contemporary information systems (such as embedded systems or service oriented architectures).

PostDoc


Pablo Picazo-Sanchez

My research interests range from computer security to applied cryptography. Over the last years I have worked on a number of areas in these fields, including: Attack modeling or Security on RFID systems.

PostDoc


...
Thomas Sewell

My research focuses on Translation validation and checking correctness of program compilations.

PostDoc


...
Jesús Mauricio Chimento

My research interests focus on studying Formal Methods, Certified Programming and Functional Programming. Regarding Formal Methods, I am keen on studying Program Specification and Program Verification, in particular Theorem Proving and Runtime Verification.

PhdStudent alumni


...
Simon Robillard

first-order theorem proving and its applications to program verification, more specifically my research interests are: Automated reasoning, Theorem proving, program verification, Type theory and Parallel programming.

PhdStudent alumni


Giuseppe Perelli

My main interest is in Logic and Formal Methods for AI. In particular: Formal specification, verification, and synthesis of multi-agent systems; Equilibtium checking and Rational synthesis for infinite duration games; Logics for games and strategic reasoning, multiplayer games, imperfect information, incomplete information; Quantitative reasoning in games; Distributed Systems; Game theory for computer science

PostDoc


...
Hanaa Alshareef

I work on verification on information privacy.

PhdStudent



...
Andreas Lööw

I am working in interactive theorem proving (HOL4, to be precise) and hardware verification.

PhdStudent


...
Oskar Abrahamsson

Together with Magnus Myreen and Andreas Lööw, Alejandro Gomez, my research focuses on CakeML and verified compilation stack.

PhdStudent


...
Alejandro Gómez Londoño

Together with Magnus Myreen and Andreas Lööw, Oskar Abrahamsson, my research focuses on CakeML and verified compilation stack.

PhdStudent


...
Claudia Cauli

My interests fall into the field of theoretical computer science, including all those areas that make use of mathematical techniques and logics, like formal methods, automata theory, computability theory, and verification.

PhdStudent


...
Raúl Pardo

My research is focused on developing rigorous techniques to design, analyse and build software to protect online privacy. My interests lie at the intersection of formal methods, online privacy and computer security. Currently, I am working in the following topics:Formal models for privacy, Verification of smart contracts, Algorithm transparency

PhdStudent alumni


...
Carlo Furia

My research is in the area of formal methods for software engineering. These include a wide array of models, techniques, methods, and tools to support the analysis, rigorous development, and verification of software and software-intensive systems.

faculty alumni


...
Yu-Ting Jeff Chen

I work on automated program verification using Intermediate Verification Languages.

PhdStudent