Semantics of Programming Languages

Material

All slides are under copyright. All rights reserved.

• Introduction to Automated Software Verification
• Exercises: Solution
• Overview
• Questions & Answers (last year)

Additional material:

• CPAchecker executable (program analysis tool)
• Lab Session (Reaching Definitions, cfa.py)

  # Clone the repository from GitLab

  git clone https://gitlab.lrz.de/sosy-lab/blockseminar-semantik-ws-2024.git

  cd repository

  
  

  # Set up a virtual environment

  python3 -m venv venv

  
  

  # Activate the virtual environment

  source venv/bin/activate

  
  

  # Install ipykernel, which consists of IPython as well

  pip install ipykernel

  
  

  # Create a kernel that can use the venv inside

  python -m ipykernel install --user --name=venv

  
  

  # Install dependencies from requirements.in

  pip install -r requirements.in

  
  

  # Run Jupyter Lab to open the notebook

  jupyter-lab

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

People

• Speaker: Matthias Kettl

The first part of the lecture was spoken by Prof. Dr. Alexander Knapp .