Semantics and Verification: Meaning and correctness in computing
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.
Overview
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 member
- Parosh Abdulla (also see his homepage): semantics, program verification, concurrency
- Mohamed Faouzi Atig: program verification, weak memory models
- Johannes Borgström: semantics, program verification, process calculi
- Lars-Henrik Eriksson: formal methods methodology, industrial applications
- Bengt Jonsson (also see his homepage): semantics, program verification, concurrency
- Joachim Parrow (also see his homepage): process calculi
- Björn Victor: process calculi
- Tjark Weber (also see his homepage): theorem proving
Research awards
- CAV Award 2017: Parosh Aziz Abdulla and Bengt Jonsson
- LiCS Test-of-Time Award 2016: Parosh Aziz Abdulla and Bengt Jonsson