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
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