Formal Specification and Verification

Lecture

Tuesday, 12:00c.t-14:00, Raum E 427
  • Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
  • Sprechstunde: Mi, 16:00

    • Exercise

  • Thursday, 12:00c.t.-14:00, Room K 107

    • Slides

    Exercises

    News

  • Exam (Termin 1): Tuesday, 17.07.2012, starting from 12:15, Room 225 (oral examination)
  • Please register to the exam using KLIPS.
    Registration for the exam is open until Monday, 16.07. 2012.
    Some remarks on registration (in German) can be found here.
  • A summary of topics for the exam is available here. updated on 11.07.2011
  • Question/Answer session 1: Thu, 12.07.2012, at the end of the exercise
  • Exam (Termin 2): Tuesday, 14.08.2012, starting from 13:00, Room 225 (oral examination)
  • Please register to the exam using KLIPS.
    Registration for the exam is open until Monday, 13.08. 2012.
  • If you have any questions please send them by e-mail to sofronie@uni-koblenz.de
  • There is no exercise due to public holiday on June 7th; the next exercise takes place on Thursday, 14.06.2012.
  • There is no exercise due to public holiday on May 17th (Ascension Day)
  • In the exercise on Thursday, 10.05.2012 I will present OBDDs (ordered binary decision diagrams) and their properties
  • Next exercise takes place on Thursday, 3.05.2012
  • There is no lecture due to public holiday on May 1st.

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