The division is divided into four units that pursue research and education that advances the design of secure and trustworthy software and systems, from theoretical foundations, and up through the design and implementation of programming languages and tools.
Formal methods
The group conducts research in the use of mathematical and logic-based techniques for the specification and verification of systems. The group is best known for its work on (automatic and interactive) theorem proving, deductive verification, verified compilation, reactive synthesis from temporal logic, runtime verification, and formal analysis of normative systems.
Functional programming
The group focuses on the application of programming technology, and functional programming techniques, in particular, to solve practical problems. The group is best known for its work on domain-specific languages, hardware verification, software testing, and (formal and natural) language technologies. Their research has resulted in two spinoff companies in addition to research publications.
Information security
The group conducts research in security and privacy, language-based security, data privacy using a range of techniques, such as differential privacy and privacy-preserving location services. The group is known for its work on information flow security, web security, and security foundations. The group is a part of Chalmers Security Lab.
Logic and types
The focus of the group is on dependent type theory, both theoretical investigations of syntax and semantics, and the implementation and applications of proof assistants. The group is best known for the development of well-known proof assistants, including the Agda system, and for several key contributions to the design and metatheory of dependent type systems.
