SEFM Summer School 2022

Affilitated with the SEFM’22

Dates and Location

21.9. - 24.9.2022

The school will start on Wednesday, 21.9., at 9am; the school will close on Saturday, 24.9. at 5.30pm. On Friday, 23.9., there will be a Summer School Dinner (included in the fees). Each of the four courses will consist of about 6 lectures of 50mins duration.

Johann von Neumann-Haus, Rudower Chaussee 25, Adlershof, Berlin, Germany

Room: Humboldt-Kabinett

Courses

Course Descriptions

Software Verification (Dirk Beyer)

The goal of the lectures is to bridge the gap between verification research and software engineering. Consequently, the lecture starts with theory and concepts, continues with a unifying view on several different verification algorithms, and finally addresses some practical problems that occur in software verification. First, we give an introduction of the framework of configurable program analysis. Second, we consolidate knowledge and show how to express four different software-verification algorithms in one unifying framework: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. We also shed light on practical aspects of software model checking and explain verification witnesses, combination approaches, and cooperative verification.

Reading Material:

Security Testing (Eduard Enoiu)

Industrial software is subject to numerous vulnerabilities. Nevertheless, several techniques exist to prevent and detect software flaws. This crash course introduces students to basic and advanced approaches to testing trustworthy industrial control systems by focusing on the interplay between security and safety. Various test techniques will be covered, along with fault detection aspects and the bindings on software security.

Design and Verification of Reliable Autonomous Systems (Michael Fisher)

Aim is to cover the software engineering, and particularly verification techniques, that might be used in developing trustworthy autonomous systems. The draft content of the lectures is as follows:

  1. Autonomous Systems: what is Autonomy; why it is different; requirements and specifications; applications and issues; regulation and standards.
  2. Architectures and Transparency: modularity and heterogeneity; systems architectures and agents; importance of transparency.
  3. Verification (static): heterogeneous verification; model-checking critical components; from “what” to “why”; dealing with opaque components.
  4. Verification (dynamic): change and the need for run-time verification; certification and verification assumptions; putting it all together; remaining issues

Much of the material is from a forthcoming book on “Verifiable Autonomous Systems” by Louise A. Dennis and Michael Fisher (due to be published by Cambridge University Press in 2022).

Designing Self-adaptive Systems (Danny Weyns)

In this course, we will introduce the basis principles of self-adaptive systems. Next, we will outline key milestones of research in this area and highlight the relevance of self-adaptation in practice. Then, we elaborate on runtime techniques that enable self-adaptive systems to provide guarantees that the systems comply with their goals while dealing with uncertainties that are difficult to anticipate at development time. The course concludes with an outline of open challenges in this interesting field of research.

Reading material:

CVs of the Lecturers

Dirk Beyer is a Full Professor of Computer Science and has a Research Chair for Software and Computational-Systems Engineering at LMU Munich, Germany (since 2016). Before, he was Full Professor of Computer Science at University of Passau, Germany (2009-2016). He was Assistant and Associate Professor at Simon Fraser University, B.C., Canada (2006-2009), and Postdoctoral Researcher at EPFL in Lausanne, Switzerland (2004-2006) and at the University of California, Berkeley, USA (2003-2004), in the group of Tom Henzinger. Dirk Beyer holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is architect, designer, and implementor of several successful tools. For example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two well-known and successful software model checkers.

Eduard Enoiu is a Senior Lecturer at Mälardalen University in Sweden. Previously, he worked at Bombardier Transportation in Sweden as a testing tool engineer and industrial Ph.D. researcher. Eduard received his Ph.D. from Mälardalen University in automatic test generation and fault detection evaluation. His current research interest is the automatic discovery of flaws and vulnerabilities in industrial control software. In addition, his interests span software engineering and empirical research, especially testing, maintaining, evolving, and assuring industrial software. He has developed, helped in the development, or led the construction of several tools that have discovered bugs in industrial control systems.

Michael Fisher is a Professor of Computer Science and Royal Academy of Engineering Chair in Emerging Technologies at the University of Manchester, UK. His research covers the verification and trustworthiness of autonomous systems, and he works with applications across nuclear robotics, offshore vehicles, space robotics, and domestic robotic assistants.

He is co-chair of the IEEE Technical Committee on the Verification of Autonomous Systems, is member of both the British Standards Institution (BSI) AMT/10 committee on Robotics and the IEEE P7009 committee on Fail-Safe Design of Autonomous Systems, and chairs the BSI committee on Sustainable Robotics.

Danny Weyns is a professor at the Katholieke Universiteit Leuven, Belgium. He is also affiliated with Linnaeus University Sweden. Danny’s research interests are in engineering self-adaptive software systems. Such systems are equipped with a feedback look that enables them to deal with uncertain operating conditions, such as dynamics in the availability of resources, workloads that are difficult to predict and user goals that change on the fly. The focus of Danny’s current research is on ensuring trustworthiness of self-adaptive systems, with validation in the domain of the Internet of Things.

Fees

500 Euro (including lunch and refreshments and a summer school dinner)

Registration

Registration is via the SEFM-Webpages

Adapted Timetable (as, unfortunately, Eduard Enoiu is unable to come to Berlin)

Time Wednesday, 21.9. Thursday, 22.9. Friday, 23.9. Saturday, 24.9.
9.00 Self Adaptive S Self Adaptive S RA Systems RA Systems
10.00 Self Adaptive S Self Adaptive S RA Systems RA Systems
11.00 – Coffee – – Coffee – – Coffee – – Coffee –
11.30 SW Verification Q&A: Career Advice SW Verification SP Analysis
12.30 – Lunch – – Lunch – – Lunch – – Lunch –
14.00 Formal Methods Self Adaptive S SW Verification SP Analysis
15.00 Self Adaptive S RA Systems Student Presentations SW Verification
16.00 – Coffee – – Coffee – – Coffee – – Coffee –
16.30 RA Systems SW Verification SP Analysis Discussion & Closing

SW Verification - Software Verification (Dirk Beyer)

RA Systems - Design and Verification of Reliable Autonomous Systems (Michael Fisher)

Self Adaptive S - Designing Self-adaptive Systems (Danny Weyns)

Formal Methods (Markus Roggenbach)

SP Analysis - Security Protocol Analysis (Markus Roggenbach)

Director and Contact

Markus Roggenbach (Swansea University, UK), email: M.Roggenbach@swansea.ac.uk