Computing Science

Image 1 of 1
Computing Science

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


Computer Science and Engineering, a joint department between Chalmers and the University of Gothenburg.