Summer School
UNU/IIST - IFIP WG 2.3



Formal Models of Software

31 August - 6 September 2003

Ecole Polytechnique de Tunisie (EPT)

Report in word format   Report in pdf format


This school presents formal models used for software development and their properties. It focuses on formal approaches for software specification and verification using programming logical foundations. Moreover, the use of these approaches for object-oriented software specification and verification is dealt with. Cryptographic protocols security is also addressed in this School. Courses are illustrated by demos using specification and verification tools.

"Refinement Calculus - Foundations and Applications"
Ralph Back, Abo Akademi, Finland

"Unifying Models and Engineering Theories of Software Systems"
Slides Available
Manfred Broy, TU Munich, Germany

"Reasoning about asynchronous programs", "Reasoning about security"
Ernie Cohen, Microsoft, USA

"Technologies for finding errors in object-oriented software"
Slides Available
Rustan Leino, Microsoft, USA

"Fault-Tolerant and Real-Time Systems: Specification, Verification, Refinement and Scheduling"
Slides Available
Zhiming Liu, UNU/IIST