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 common theme of the unit is the application of mathematics and logic to different aspects of theoretical computer science.
One research topic is theoretical and practical aspects of dependent type theory, including the implementation of proof assistants such as Agda, homotopy type theory, synthetic algebraic geometry and the application of type theory to quantum computing.
Another research topic is algorithmic graph theory, in particular NP-hard graph-theoretic problems.
For more information about the research in the unit, please visit Logic and types' web page.
