Formal Specification and Verification

Lecture

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

  • Exercise

  • Thursday, 12:00c.t.-14:00, Room E 524 (every 14 days, start: 25.04.2013)

  • Slides

    Exercises


    News

  • Exam
  • Termin 1: Thursday, 25.07.2013, Room B 225 (oral examination)
    • Please register to the exam using KLIPS.
    • Registration for the exam is open until 25.07. 2013
    • A summary of topics for the exam is available here
  • Question/Answer session 1: Wed, 24.07.2013, 11:00, Room B 225

  • Termin 2: 14.08.2013, 11:00, Room B 225 (oral examination)
    • Registration enabled
  • Question/Answer session 2: Monday, 12.08.2013, 14:00, Room B 225
    If the time does not suit you but you have questions please send me an e-mail (E-Mail address: sofronie@uni-koblenz.de)

  • Thu, 13.06.2013: exercise (Matthias Horbach)
  • Tue, 11.06.2013: exercise (Matthias Horbach)
  • No exercise on Thu 09.05.2013 (Christi Himmelfahrt)
  • On Tue 07.05.2013 instead of the lecture an exercise is scheduled.
  • No exercise on Thu 30.05.2013 (Fronleichnam)
  • On Tue 28.05.2013 instead of the lecture an exercise is scheduled.

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