# Formal Specification and Verification

### Lecture

Tuesday, 12:00c.t-14:00, Raum E 427

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.