In this paper we describe and review the course plan and syllabus we use in
a course on formal methods in software engineering currently included in t
he degree in Informatics of the Faculty of Sciences at the University of Bo
logna. The course matches the theory of formal methods with their practice
based on actual tool usage. In fact, the course is centered upon a project
whose main goal is to let students learn some formal specification techniqu
es, all supported by specific tools. The students use well-known notations
for both requirements specification and formal design. The formal methods w
e use are based on the Z notation for requirements specification and on the
Larch family of languages for design specifications.