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.


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.


Moa Johansson

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


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.


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.


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