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
I am a PostDoc Researcher at the Dept. Of Computer Science and Engineering, affiliated under Göteborg Universitet. I have been a research associate at the University of Leicester and since then I am working on the ERC consolidator grant D-SynMA (led by Prof. Nir Piterman), investigating distributed reactive synthesis for Multiagent Systems. I was a PostDoc Researcher at SysMA research unit in IMT School for Advanced Studies Lucca, Italy; also a member of the Italian Project FILIERASICURA with Cisco Italia. I obtained my PhD degree, as well as the *Doctor Europeaus* certificate from IMT School for Advanced Studies Lucca working towards a Foundational theory of collective-adaptive systems. During my PhD, I have been a visiting research scholar at the Dept. Of Informatics, LFCS Laboratory in the University of Edinburgh where I investigated Quantitative Analysis of collective-adaptive systems.
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
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