Course: Formal Methods
Eindhoven University of Technology, Eindhoven
June 11 – 15, 2018
Update 2018/06/14: the slide sets for Anton Wijs and Muhammad Osama’s Tuesday afternoon course part, and for all of Marijn Heule’s and Michel Reniers’s course components have been added.
IPA organises Advanced Courses on each of its major research fields: Algorithmics and Complexity, Formal Methods and Software 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, with some prominent international speakers as well. From several of these areas, such as SAT solving and certification, model checking, verification, supervisory control, and graph transformation, topics are taken and treated in one or one and a half course days each. Course components consist of lectures mixed with active training (exercises, assignments, etc.).
Dates, Location and Programme
The lectures will take place in room MF 6.131 on floor 6 of building Metaforum at the TU/e campus. 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.
| MONDAY 11 June and TUESDAY MORNING 12 June |
Marijn Heule (University of Texas at Austin) |
| Propositional proofs — Theory and practice
Satisfiability (SAT) solvers are used for determining the correctness of hardware and software systems. It is therefore crucial that these solvers justify their claims by providing proofs that can be independently verified. This holds also for various other applications that use SAT solvers. Just recently, long-standing mathematical problems were solved using SAT, including the Erdos Discrepancy Problem, the Pythagorean Triples Problem, and Schur Number Five. Especially in such cases, proofs are at the center of attention, and without them, the result of a solver is almost worthless. What the mathematical problems and the industrial applications have in common, is that proofs are often of considerable size—in the case of the Schur Number Five about 2 petabytes. As the size of proofs is influenced by the strength of the underlying proof system, the search for shorter proofs goes hand in hand with the search for stronger proof systems. The tutorial will cover both the theoretical and practical aspects of proof production and validation as well as an introduction in strong proof systems that can compactly express the broad spectrum of techniques used in SAT solvers. Slide sets: 1 2 3 4 5 |
|
| TUESDAY AFTERNOON 12 June and WEDNESDAY 13 June |
Marieke Huisman and Sebastiaan Joosten (UT) and Anton Wijs and Muhammad Osama (TU/e) |
| GPU computing — Development and analysis
GPU computing is becoming more and more mainstream. The massive parallellism that is provided by GPUs provide new opportunities, but also new challenges, for speeding up many different kind of applications. During these lectures, we will first introduce you to the GPU programming model, and you will get to write your own application. Then we will discuss techniques to reason about the behaviour of GPU applications, i.e. how to prove deadlock, divergence freedom and functional correctness, and you will get to try this on various applications – including the application you developed yourself. The training will be concluded with a presentation of various advanced GPU applications, in particular how model checking algorithms can be ported to the GPU. Slide set for Tuesday afternoon: 1 |
|
| THURSDAY 14 June | Michel Reniers and Asia van de Mortel-Fronczak (TU/e) |
| CIF 3: Model-based Engineering of Supervisory Controllers The engineering of supervisory controllers for large and complex cyber-physical systems requires dedicated engineering support. The Compositional Interchange Format language and toolset have been developed for this purpose. We highlight a model-based engineering framework for the engineering of supervisory controllers and explain how the CIF language and accompanying tools can be used for some of the typical activities in that framework such as modeling, supervisory control synthesis, simulation-based validation, verification, and visualization, real-time testing, and code generation. We mention a number of case studies for which this approach was used in the recent past. We discuss future developments on the level of language and tools as well as research results that may be integrated in the longer term. Slide set |
|
| FRIDAY 15 June | Leen Lambers (Hasso Plattner Institute) |
| Graph Transformation – Theory and Practice
Graphs are omnipresent as a data structure in computer science. Graph transformation (GT) describes the rule-based manipulation of graphs. This tutorial starts with an overview of GT application fields and some respective case studies. We continue with introducing the basic theoretical building blocks of GT illustrated by a simple running example. We then move on to more complex modeling features (such as typing, attributes & graph conditions) needed for GT to be successfully applicable in practice. We conclude this tutorial with reviewing some GT analysis techniques and how they help solving significant problems in the earlier introduced GT application fields and case studies. Pen and paper exercises support the understanding of GT theory and a tool session illustrates the practical use of GT. |
Social
On Monday June 11th, the course will be followed by IPA-sponsored drinks and snacks at de Zwarte Doos on the TU/e campus—17:00-18:30.
Registration
Registration closed on Thursday May 31st.
Accommodation
Unlike for IPA’s 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, let us know and we will provide basic overnight accommodation. You can specify your accommodation needs on the registration form.