Formal Specification and Verification
Lecture
- Tuesday, 12:00c.t-14:00, Raum E 427 (weekly)
- Thursday, 12:00c.t-14:00, Raum E 524 (every 14 days, start: 18.04.2013)
Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
Exercise
News
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.