Skip to main content
Department of Information Technology

Semantics and Verification

Meaning and correctness in computing

Overview

Semantics concerns the exact meaning of programming languages and other notations such as design descriptions. Semantics is important to precisely understand and describe the behaviour of computer programs and ensure they work the same on different computing platforms.

Verification concerns demonstrating the absence of bugs in programs and the correctness of models of computer systems. Formal verification can -- in contrast to testing -- in principle guarantee the correct behaviour of a program.

Semantics and verification are of particular importance with concurrent and parallel systems as such systems are inherently complex and are prone to have mistakes and hard-to-find bugs. A good example is memory handling in multi-core processors.

We develop theories and methods for various aspects of semantics and verification. Formal logic and systems for computer-assisted mathematical proof (theorem-proving systems) are important tools.

Research Topics

  • Concurrency
  • Formal methods methodology
  • Process calculi
  • Program verification
  • Semantics
  • Testing
  • Theorem proving
  • Weak memory models
  • Industrial applications

Faculty Members

Courses

  • 1DT034: Programming Theory
  • 1DT311: Semantics of Programming Languages
  • 1DT610: Software Testing
Updated  2022-06-13 13:16:51 by Lars-Henrik Eriksson.