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
  • Friday, 10:00-12:00, A 213 (every second week)

    • Slides

    Exercise Sheets

    Lecture under OLAT

    Forum under OLAT

    Exam:

  • Termin 1: Friday, 8.03.2024 (probably oral)

    The registration in KLIPS is open since Mo, 22.02.2024. Registration is possible until 1.03.2024; you can deregister until 2.03.2024.

  • 2. Termin: There will be two possibilities of repeating the exam:

    • News

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

    1st exercise session: Friday, 10.11.2023

    2nd exercise session: Friday, 17.11.2023 (one hour exercise, one hour lecture)

    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

    For the exam, the slides and the material provided in electronic form on the wensite of the lecture will be sufficient.

    Additional references for the area "Formal specification/Formal verification" are listed below:

  • 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.