Menu:  Organization    Program (PDF)  tinynew.gifProceedings   Concept   Submissions    Repository 

Formal Methods in the Teaching Lab

Examples, Cases, Assignments and Projects
Enhancing Formal Methods Education

A Workshop at the Formal Methods 2006 Symposium
Workshop: Saturday, August 26, 2006
Symposium: August 21 - 27, 2006
McMaster University, Hamilton, Ontario, Canada

Formal Methods Europe
Formal Methods Europe


This workshop is organized by the Formal Methods Europe Subgroup on Education.

Workshop Co-Chairs

Raymond Boute
Formal Methods Group, Department of Information Technology (INTEC),
Ghent University, Ghent (Belgium)

José Oliveira
Departamento de Informatica
Universidade do Minho, Braga, Portugal

Program of the Workshop

9h00 - Tool Support for Learning Buchi Automata and Linear Temporal Logic, by Yih-Kuen Tsay, Yu-Fang Chen, and Kang-Nien Wu
9h30 - Supporting Formal Method Teaching with Real-Life Protocols, by Hugo Brakman, Vincent Driessen, Joseph Kavuma, Laura Nij Bijvank and Sander Vermolen
10h00 - A Playful Approach to Formal Models, by Katharina Spies, Bernhard Schaetz
11h00 - Two courses on VDM++ for Embedded Systems: Learning by Doing, by Peter Gorm Larsen
11h15 - Comments on several years of teaching of modelling programming language concepts, by J W Coleman, N P Jefferson, and C B Jones
11h30 - A Graduate Seminar in Tools and Techniques, by Patrick J. Graydon, Elisabeth A. Strunk, M. Anthony Aiello, and John C. Knight
11h45 - Teaching the Mathematics of Software Design, by Emil Sekerinski
12h00 - Basic Science for Software Developers, by David Lorge Parnas and Michael Soltys
12h15 - Introducing Model Checking to Undergraduates, by Abhik Roychoudhury
14h00 - Evaluating a Formal Methods Technique via Student Assessed Exercises, by Alastair F. Donaldson and Alice Miller
14h15 - Enhancing student understanding of formal method through prototyping, by Andreea Barbu and Fabrice Mourlin
14h30 - From Run-time Analysis to Static Analysis of Java Programs: A Teaching Approach, by Christelle Scharff and Sokharith Sok
14h45 - The Use of an Electronic Voting System in a FM Course, by Alice Miller and Quintin Cutts
15h00 - Teaching with the Computerised Package Language, Proof, and Logic (LPL), by Roussanka Loukanova
15h45 - FORUM

Proceedings of the Workshop

  • Electronic proceedings (1.4Mb PDF)
  • Slides of all presentations

Concept of the Workshop


Quoting Dines Bjørner:
    “Formal Methods Education is currently facing a ‘trichotomy’.
  • On the one hand, industries dealing with the design of complex and critical systems have an increasing need for methods that provide a certain degree of confidence in the result, and are often looking for external assistance in the area of formal methods from consulting companies and academia.
  • On the other hand, a growing number of university staff enjoys the intellectual challenge of research in this area and teaching formal techniques to students.
  • On the ‘third hand’, an increasing number of students de-select formal methods in the curriculum, due to various causes and trends.”
One cause of the problem is a general mathphobic trend in society and education.
     Another cause is that, intellectually, Information Technology is the victim of its own success. Indeed, the rapid growth creates so many design and implementation tasks that can be done and, more importantly, are being done with negligible educational or scientific background that it is difficult to argue convincingly in favor of formal methods on the basis of immediate everyday necessities. Critical systems, of course, are a notable exception.
     These trends are so pervasive that the small minority of FM educators has little hope to curb them in the near future. More effective in the long term is instilling a higher degree of professionalism in the next generation. This requires in particular a directed, positive action towards motivating students.


This workshop solicits short papers, presentations, demonstrations and evaluations describing sharp classroom or lab experiments which have proved particularly beneficial to the students' understanding and motivation for formal methods.
     The emphasis is not on (new) theories or methods but on specific illustrations and exercises that can be used by colleagues in their own courses, perhaps applying their own formalisms.
     The main goals are:
  • to share knowledge and experience on the practicalities of teaching and learning formal methods;
  • to build a collection of interesting cases, examples, assignments and projects that FM teachers can use in educational activities.


The workshop will be a forum-like event, with short presentations, demos and informal discussion slots. After the workshop, if the evaluation committee decides that there is a sufficient number of high-quality submissions, an agreement will be sought with Springer Lecture Notes in Computer Science about publishing a special volume, and authors will be invited to submit their contribution for refereeing.


Call for Contributions

This workshop solicits papers, presentations, demonstrations and evaluations describing such material in detail and how it has been beneficial to the students' understanding and motivation.
     The emphasis should not be primarily on new theories or methods but on specific illustrations and exercises that can be used by colleagues in their own courses, perhaps applying their own formalisms.
     The central problem(s) should be clearly stated and a typical solution outline provided (using the author's preferred method), accompanied by a discussion of what educational aspect is meant to be enhanced. Contributors should motivate their techniques with a discussion of the desired knowledge and skill outcomes of the examples/case studies or projects, and a frank appraisal of their effectiveness, insofar as such an appraisal is meaningful and instructive, which we expect to be the case for most topics.
     Papers should be kept short (maximum 6 pages). They should be prepared preferably in LaTeX, and a pdf-file should be sent to Submitted papers will be evaluated by the Subgroup on Education.


   Submission deadline:   Friday, June 9, 2006

   Acceptance notification:   Saturday, July 1, 2006

Repository and follow-up

The organization will produce a web-based resource of output from the workshop housed under Contributors willing to allow their teaching materials to be made publicly available for the community are invited to send source files, links or tools and other information that would be suitable for such an on-line repository, which the organization will keep alive on a wiki-like basis.
     The collected material will form the start of a compendium of examples, cases, assignments and projects, according to the following (rough) categorization.

  • Examples are shorter items, ranging in length from a single observation to over a full page. An example is aimed at clarifying a single aspect where the essence is captured in a somewhat condensed form, with minimal clutter from side-issues.
  • Cases are taken from situations encountered in practice, where the problems may appear in various forms: from immediately appealing (and hence motivating) but not very challenging to subtly hidden and requiring major research. Side-issues and secondary problems may be included to clarify the setting or to illustrate the need for abstraction.
  • Assignments and projects correspond to examples and cases respectively, but the difference is that they are elaborated by the students rather than the instructors.
The repository is expected to evolve in at least 3 dimensions:
  • new items are added in their original form as time proceeds;
  • existing items are reworked in various formalisms;
  • experience in teaching is reported.
Every one or two years, people who submit the most suitable contributions will be invited to join forces for combining their work into a "laboratory notebook".
     Any further suggestions are welcome.

 Valid HTML 4.01!  
Author: Raymond Boute