Formal Specification and Verification

Lecture

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

  • Exercise

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

  • Slides

    Exercise Sheets


    Exam

  • Termin 1: Thursday, 7.08.2014, Room B 225 (oral examination)
  • Question/Answer session 1: Tue, 5.08.2014, 11:00, Room B 225

  • Termin 2: September 2014, TBA, Room B 225 (oral examination)

  • News

  • 8.07.2014: The lecture is held by Matthias Horbach
  • 22.05.2014: This session starts with the discussion of the exercises;
    afterwards we may continue with the lecture (depending on the time we need for the exercises)
  • 20.05.2014: The lecture is held by Matthias Horbach
  • 15.05.2014: Exercises
  • 13.05.2014: Lecture
  • 8.05.2014: Exercises
  • 6.05.2014: Lecture
  • 1.05.2014: free day
  • 29.04.2014: Lecture
  • 24.04.2014: Lecture
  • 22.04.2014: Lecture

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