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

  • Thursday, 14:00-16:00, Room E 113 (every 14 days)

  • Slides

    Exercise Sheets


    Exam

  • Termin 1: Thursday, 9.03.2017, 10:00s.t.-12:00 Room M 001 (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)

  • Question/Answer session: Tuesday, 7.03.2017, 14:00-16:00, Room B 016

  • Termin 2: 3.04.2017, Room B 225 (oral exam, the exact times will be communicated by e-mail)

    For an oral exam you cannot use an A4 sheet with notes.
    I will provide information about logical calculi
    (Axioms + Deduction rules, Rules in the sequent calculi)
    which you can use during the exam.


  • News

  • The lecture on Thursday 14:00-16:00 takes place in Room E 113.
  • The lecture on Tuesday 10:00-12:00 takes place in Room K 107.

  • Contents

  • Introduction
  • Specification
  • Logic (Classical logic; Temporal logic)
  • Selected specification languages
  • Basics of Deductive Verification
  • Hoare Logic and Dynamic Logic
  • Decision procedures for data types
  • Model Checking
  • 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.