Software Verification: Contracts, Trusted Components and Patterns

Bertrand Meyer, Manuel Oriol, Till Bay (Fall semester 2008)


General info: News | Course description | Grading | Course books | Downloads | Further reading | Exam | Wiki
Lectures: Subjects and Slides

General info


31.08.2008 Website up and running, tentative schedule added.
29.09.2008 The exercises are available for Exercise Session 1.
06.10.2008 The exercises are available for Exercise Session 2.
28.10.2008 The project description is available.

Course description

Software Verification: Contracts, Trusted Components, and Patterns

Web page at the computer science department: 251-0239-00 (3G)

Trusted Components are reusable software elements accompanied with a guarantee of quality. They should be equipped with contracts describing their abstract properties. The course explores the various facets of this notion. Topics include: the notion of software quality; library design; the notion of design pattern, and whether patterns can be turned into components ("componentization"); program correctness and axiomatic semantics; testing; techniques of program analysis, model checking, abstract interpretation; proof-carrying code.


The project (a take-home exercise) will contribute 30% to the overall grade. A written exam on 15 December (during the usual lecture time) will contribute the remaining 70%.

Course books

  • Research articles may be required to read during the course.
  • Eiffel Tutorial
  • Bertrand Meyer: Object-Oriented Software Construction, Second Edition, Prentice Hall, 1997 ISBN 0-13-629155-4
Other (recommended) books:
  • Robert V. Binder: Testing Object-Oriented Systems: Models, Patterns, and Tools, Addison-Wesley, 1999.
  • Karine Arnout: From Patterns to Components, Ph.D. thesis, 2004. (See downloads)
  • Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides: Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, 1995, ISBN 0201634988
  • Richard Mitchell, and Jim McKim: Design by Contract, by Example, Addison-Wesley, 2001, ISBN 0201634600


  • EiffelStudio 6.0 Free Edition is available for Windows, Linux, and MacOS. Click here!
  • Arnout's Component library for Design Patterns. Click here!

Further reading

About Eiffel and O-O programming:

  • Karine Arnout: Eiffel: The Essentials, 2004 (Appendix A of Ph.D. dissertation From Patterns to Components).
  • Peter Thomas, Ray Weedon: Object-Oriented Programming in Eiffel, Second Edition, Addison-Wesley Eiffel in Practice Series, ISBN 0-201-33131-4.
  • Frieder Monninger: Eiffel. Objektorientiertes Programmieren in der Praxis, H. Heise Verlag, Hannover, ISBN 3-882-29028-5
  • Bertrand Meyer: La produzione del software object oriented. Prentice Hall International, Hemel Hempstead, ISBN 88-256-0205-7
  • Giuseppe Callegarin: Nuovo corso di informatica. Basi di dati e sistemi informativi. Per le Scuole superiori.CEDAM, ISBN 8-813-19565-6
  • Karine Arnout's Ph.D. thesis: From Patterns to Components. Click here!

About Program Analysis:


Stephan van Staden is the organizing assistant for the course. Please contact him if you have any questions.





Monday 9:00-11:00 RZ F21
Wednesday 10:00-11:00 RZ F21



Previous exams:


Week by Week Schedule