Formal Specification and Verification

Lecture

  • Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
  • Sprechstunde: Mo. 16:00-17:00 (please send an e-mail before)

    • Exercise:

    Viorica Sofronie-Stokkermans
  • Thursday, 16:00s.t.-17:00, online (every week)
    online Conference system Big Blue Button (BBB) under OLAT (Gruppe "Formal Specification and Verification WS 2021/22)

    • Slides

    Exercise Sheets

    Forum under OLAT (Group "Formal Specification and Verification WS 2021/22")

    Exam:

  • Termin 1: Thursday, 10.03.2022, 11:00s.t.-13:00 Room M001 (written exam, 120 min.)

    You are allowed to use an A4 sheet with notes you made about the lecture
    (written on both sides, written by you, and marked with your name)

  • Termin 2: Thursday, 21.04.2022 (written or oral exam, depending on the number of participants).

    • News

    (latest news first) The first exercise sheet will be available online on Friday, 29.10.2021.

    The first exercise session will take place on Friday, 5.11.2021 (BBB in OLAT)

    A first online meeting is planned for Friday, 29.10.2021 (BBB in Olat).
    It will be a brief meeting, in which we will discuss organisatoric aspects.

    The audio-commented slides for the first lecture will be available
    in Panopto at latest on Wednesday, 27.10.21 at 10:00.
    (The slides will be available from the website of the lecture.)

    The audio-commented slides for the second lecture will be available
    in Panopto at latest on Friday, 29.10.21 at 10:00.
    (The slides will be available from the website of the lecture.)

    Infos on slides/meetings

  • 27.10.2021: Slides and Links to audiocommented slides available here
  • 29.10.2021: Slides and Links to audiocommented slides available here
  • 03.11.2021: Slides and Links to audiocommented slides available here
  • 10.11.2021 and 11.11.2021: Slides and Links to audiocommented slides available here
  • 17.11.2021 and 18.11.2021: Slides and Links to audiocommented slides available here 24.11.2021 and 25.11.2021: Slides and Links to audiocommented slides available here 1.12.2021 and 2.12.2021: Slides and Links to audiocommented slides available here

    • Contents

  • Introduction
  • Specification
  • Logic (Classical logic; Temporal logic)
  • Selected specification languages
  • Basics of Deductive Verification
  • Model Checking
  • Hoare Logic and Dynamic Logic
  • Deductive Verification; verification by abstraction/refinement; ...

    • Literature

  • Jose Bacelar Almeida, Maria Joao Frade, Jorge Sousa Pinto and Simao Melo de Sousa. Rigorous Software Development: An Introduction to Program Verification, Springer Verlag, 2011.
  • Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
  • Christel Baier and Joost-Pieter Katoen. Principles of Model Checking, The MIT Press 2008.
  • Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.
  • Peter H. Schmitt. Formal Specification and Verification. Skriptum zur Vorlesung. Universität Karlsruhe, 2005.