Course: Formal Methods

Eindhoven University of Technology, Eindhoven
28 October-1 November, 2013

IPA organises Advanced Courses on each of its major research fields: Algorithmics and Complexity, Formal Methods and Software Engineering and Technology. Each of these Advanced Courses intends to give an overview of (part of) the research of IPA in this specific field.

The Advanced Course, which is hosted by IPA at the Eindhoven University of Technology, focusses on subject areas in formal methods where successful research is being conducted by groups in IPA. From several of these areas, functional programming, SAT and SMT solving for (program) verification, coalgebra, cloud computing and formal methods for biology, topics are taken to which an entire course day is dedicated. Course days consist of lectures mixed with active training (exercises, assignments, etc.).

Dates, Location and Programme

The lectures will take place in room 1.105 in building Laplace of the TU/e. The overall schedule of the course is as follows: course days will start at 10.00 and last until approximately 16.30 hours. Short coffee breaks are planned at around 11.00 and around 14.45 and an organised lunch break at, roughly, 12.30-13.30. A more detailed planning and more information will be posted below in due time. The tentative agenda, including tentative topic titles, is listed below. If available, a more detailed description of the lecture will be displayed by clicking on a title.

28 October Wouter Swierstra (UU)
High assurance functional programming in Haskell
In this course you will learn to program in Haskell, an advanced purely-functional language designed specifically to allow the rapid development of concise and correct software. This course will get you started in Haskell, but also focus on several verification techniques, including automatic testing, equational proofs, and interactive theorem provers.
29 October Stefan Blom (UT), Marieke Huisman (UT) and Hans Zantema (TU/e and RU)
SAT/SMT solving for program verification
SAT(isfiability) is the very basic question whether for a given Boolean formula variables can be assigned such that the formula yields true. In extensions (usually called SMT: satisfiability modulo theories), apart from Boolean variables also number valued variables can be used, for which typically the theory includes linear inequalities over these variables. Surprisingly, problems from a wide range of applications can be expressed in SAT/SMT, and current solvers are able to solve them, up to formulas over thousands of variables. Among other application areas, this has led to significant progress in program verification, where SAT/SMT is used to automatically validate generated proof obligations.In the morning program (by Hans Zantema) some basics of SAT/SMT and its underlying technology will be presented, combined with some exercises in using the Z3 solver. In the afternoon program (by Marieke Huisman and Stefan Blom) the emphasis will be on how to apply this technology on program verification. The afternoon will end with exercises using the Dafny program verifier, emphasising the link between program annotations and generated SAT/SMT problems.
30 October Alexandra Silva (RU) and Jurriaan Rot (UL and CWI)
Coinduction at work
In this course, we will give a brief introduction to coinduction and we will illustrate how it can be used to prove language equivalence of automata. We will show enhancements to the coinduction proof method and how it can use in automated proofs. The course will consist of two lectures and two exercise sessions.
31 October Frank de Boer (CWI), Peter Wong (SDL-Fredhopper) and Behrooz Nobakht (SDL-Fredhopper)
Tentative Topic: Formal Methods for Cloud Applications
1 November Laura Bertens (UL) and Jetty Kleijn (UL)
Petri Net Modelling of Biological Processes
Formal modelling of biological processes is a crucial prerequisite for quantitative and qualitative analysis of these processes. Modelling using Petri Nets has recently gained importance in the field of bio-informatics and will be the focus of this course. The day will be structured as follows:

  • first we will discuss the role of modelling techniques in the study of biological processes and the ways in which these may contribute to our understanding, as a platform for formal analysis, simulation, or visualisation.
  • next we will focus on the framework of Petri Nets, providing a basic introduction of this methodology and illustrating how (extended) Petri Net models can be applied to faithfully represent various aspects of biological processes.
  • a biological case study will be presented; aspects of which will serve as a basis for the explanation of a tool for the construction and simulation of Petri Net models.
  • finally, as a practical assignment, the students will construct a Petri Net model for a sub-process of the previously explained case study.

The course is aimed at students interested in putting their computer science knowledge to use in the fields of biology and bio-informatics or who want to familiarize themselves with Petri Nets and their range of application. No prior knowledge of either Petri Nets or the field of biology is required.

Course Material

Course material will be handed out during the course. Where possible, this material will be made available for downloading via this page.

Costs

The courses are intended for IPA PhD students, giving them an overview of IPA’s research. For IPA PhD students, participation is free of charge (including overnight accommodation if necessary, see below), but registration is required. Other IPA-members can attend if there is capacity left, and the same holds for members of associated research schools. For these categories we will charge costs for the course material, lunches, etc, and IPA will not provide overnight accommodation. Contact us for information regarding pricing. For all categories, in case of no show extra charges may apply.

Registration

You can register using the online registration form. The form allows you to specify which course days you will attend. To make the course count as one of the required elements in the “Opleidings- en Begeleidingsplan” of an IPA Ph.D student, at least 80 percent of the course days must be attended. If you require overnight accommodation in Eindhoven for one or more nights during the course, please specify this in the “Remarks” box of the form. Registration closes on 14 October, 2013.

Accommodation

Unlike Spring Days and Fall Days, overnight accommodation is not included by default for this course. The schedule is set up in such a way that it is feasible for many students to commute. In the event this is not feasible, we will provide basic overnight accommodation.  You can specify your accommodation needs on the registration form.