Semantics of Programming Languages

This page provides material for a small part of the above-mentioned course (applications to software verification).

Material

All slides are under copyright. All rights reserved.

• Introduction to Automated Software Verification
• CPAchecker
• SMT-based Software Verification
• Verification-Result Witnesses

• Handout
• Exercises
• Exercises Solution

Additional material:

• CPAchecker executable (program analysis tool)
• Lab Session 1
• Lab Session 2

Literature

• Combining Model Checking and Data-Flow Analysis. Dirk Beyer, Sumit Gulwani, and David Schmidt. In Handbook on Model Checking, pages 493-540. Springer, 2018.
  doi:10.1007/978-3-319-10575-8_16
  Preprint
• A Unifying View on SMT-Based Software Verification. Dirk Beyer, Matthias Dangl, and Philipp Wendler. Journal of Automated Reasoning, 60(3):299--335, 2018.
  doi:10.1007/s10817-017-9432-6
  Preprint

People

• Speaker: Prof. Dr. Dirk Beyer
• Tutor: Thomas Lemberger,