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

  • Monday, 12:00-14:00, Room A 120 (every 14 days)

  • Slides

    Exercise Sheets


    Exam

  • Termin 1: Friday, 22.02.2019, 13:00s.t.-15:00 Room D 028 (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)

  • Summary of topics: list-of-topics.pdf
  • Question/Answer session: Wednesday, 20.02.2018, 13:00 c.t. -15:00, Room B017

  • Termin 2: 25.03.2019, 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


    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.