Keynote Speakers & Tutorials

You are here: Home » Keynote Speakers & Tutorials

STAF keynote

Making Model-Driven Verification Practical and Scalable: Experiences and Lessons Learned.

Verification challenges in the software industry, including testing, come in many different forms, due to significant differences across domains and contexts. But one common challenge is scalability, the capacity to test and verify increasingly large, complex systems. Another concern relates to practicality. Can the inputs required by a given technique be realistically provided by engineers? Though, to a large extent, Model-Driven Engineering (MDE) is a significant component of many verification techniques, a complete solution is necessarily multidisciplinary and involves, for example, machine learning or evolutionary computing components.
This talk reports on 10 years of research tackling verification and testing problems, in most cases in actual industrial contexts, relying on MDE but also metaheuristic search, optimisation, and machine learning. The focus of the talk will be on how to scale to large system input spaces and achieve practicality by decreasing the level of detail and precision required in models and abstractions. I will draw from past and recent experiences to provide practical guidelines and outline possible avenues of research.
Concrete examples of problems we have addressed, and that I will cover in my talk, include schedulability analysis, stress/load testing, CPU usage analysis, robustness testing, testing closed-loop dynamic controllers, and SQL Injection testing. Most of these projects have been performed in industrial contexts and solutions were validated on industrial software.

Lionel Briand

University of Luxembourg

Monday 20 July, 2015
9:00 – 10:30    (plenary session)

Lionel C. Briand is professor and FNR PEARL chair in software verification and validation at the SnT centre for Security, Reliability, and Trust, University of Luxembourg. He also acts as vice-director of the centre. Lionel started his career as a software engineer in France (CS Communications & Systems) and has conducted applied research in collaboration with industry for more than 20 years. Until moving to Luxembourg in January 2012, he was heading the Certus center for software verification and validation at Simula Research Laboratory, where he was leading applied research projects in collaboration with industrial partners. Before that, he was on the faculty of the department of Systems and Computer Engineering, Carleton University, Ottawa, Canada, where he was full professor and held the Canada Research Chair (Tier I) in Software Quality Engineering. He has also been the software quality engineering department head at the Fraunhofer Institute for Experimental Software Engineering, Germany, and worked as a research scientist for the Software Engineering Laboratory, a consortium of the NASA Goddard Space Flight Center, CSC, and the University of Maryland, USA. Lionel was elevated to the grade of IEEE Fellow for his work on the testing of object-oriented systems. He was recently granted the IEEE Computer Society Harlan Mills award  and the IEEE Reliability Society engineer-of-the-year award for his work on model-based verification and testing. His research interests include: software testing and verification, model-driven software development,  search-based software engineering, and empirical software engineering. Lionel has been on the program, steering, or organization committees of many international, IEEE and ACM conferences. He is the coeditor-in-chief of Empirical Software Engineering (Springer) and is a member of the editorial boards of Systems and Software Modeling (Springer) and Software Testing, Verification, and Reliability (Wiley).

More details can be found on:

The presentation can be found here: Slides

ECMFA Keynote

Model Patterns

What stands in the way of more widespread adoption of model-driven engineering?
There are a lot of directions in which a reasonable answer to this question may be found, but this talk addresses the hurdle that has to be overcome in getting acquainted with the available concepts and learning how to apply them to the modelling task at hand. When facing a given domain structure, what are possible ways to capture this in appropriate metamodelling concepts, and among those possible ways, what are their respective advantages and disadvantages? For instance, if your domain includes a map that associates a single element of kind B with every element of kind A, how can that particular feature be modelled? If there are multiple solutions (as indeed there typically are), how does one identify the best one for any given purpose?

To break down this hurdle, I propose to start putting together a compendium of “model patterns”, which can be used as building blocks for metamodels, fulfilling the same role that design patterns play in programming. If such model patterns are properly defined, it will become possible to apply, refactor and recognise them automatically, and reason more precisely about their benefits. To stick with the above example, a map may be represented as a simple one-to-one association from A to B, or as a special association class between A and B, or as a qualified association to B where A is the qualifier class. Ideally it should be possible to automatically migrate from a less expressive structure to a more expressive one.

During the talk I will explain and illustrate the idea of model patterns and what I believe you could do with them. The intention is to draw the audience into the discussion: what model patterns do you know? Can we already define a library of such patterns? If we succeed in getting such an initiative going, then quite possibly this will bring the widespread adoption of model-driven engineering a small step forward.

Arend Rensink

University of Twente (The Netherlands)

Wednesday 22 July, 2015
9:00 – 10:30    (plenary session)

Arend Rensink’s current main research is in model-driven engineering, in particular DSL definition and model transformation. The problems he is especially interested in have to do with correctness: when can a transformation be called correct, and how can we formally, preferably automatically, etablish correctness? To answer these questions he proposes to use graph transformation as underlying formalism, as it is suitable both for expressing the transformations and for expressing the DSL semantics that typically should be preserved. As a vehicle to demonstrate and validate his research, he has developed the tool GROOVE, which specialises in graph transformation-based state space exploration and model checking.

Arend Rensink came to this field from process algebra, in particular action refinement, in which he obtained his PhD degree in 1993 at the University of Twente. After working for 5 years at the University of Hildesheim, he returned to his alma mater, where he was appointed full professor in 2010.

More details can be found on:

The presentation can be found here: Slides

Towards MBE – a tale of 4 introductions

Model Based Systems Engineering (MBSE) serves several engineering purposes. Depending on technical background engineers appreciate the model based way of working in different ways. Models, when realized, serve to provide the view on system architectural design at a higher abstraction level. This is made with the aim to define a well-balanced top level system design. It is however not necessarily as straightforward as one could expect. The communicative part of system architecture models are not always well understood among stakeholders, nor are the design tools and methods intuitive enough for system architectural design engineers. Subsystem design activities are nominally well supported by MBSE methods. Depending on methods and process requirements however, the usage can be very well accepted, or more or less obstructed. Success factors must be more rigidly taken into account when choosing methods and tools for demanding research as well as product development projects. Factors to take into account may vary from system complexity, safety and security aspects as well as organization maturity. Modelling allows another approach to design and verification work than does traditional requirements – design – implementation – testing – verification – validation way of working. The very fast design loops with concurrency on several design levels put delicate demands on the full development system. Experiences show that MBSE maturity varies in industry as to accept new design approaches into existing Systems Engineering and Software Engineering processes. Industry design and development processes have since many years been adapted to efficiently utilize tool sets depending on technology and type of system subject to development. In making design and development activities even more efficient, new approaches must be defined, supported by tools, methods and processes, to allow for compliance to functional as well as process and regulatory requirements on design.

Sam Nicander

Saab Aeronautics

Thursday 23 July, 2015
9:00 – 10:30    (plenary session)

Sam Nicander is Systems Engineering manager at Saab AB Aeronautics. He has in most of his working career been involved in complex systems design and development. The prime area of interest is Flight Control System architecture and design, which involves making several technical disciplines and provides very high demands on rigid development processes. His MBSE knowledge is very much based on practical experiences from Saab internal, as well as, international collaboration projects.


ICGT Keynote

From Software Modeling to System Modeling – Transforming the Change

Model-driven software engineering has gained momentum in academia as well as in industry for improving the development of evolving software by providing appropriate abstraction mechanisms in terms of software models and transformations thereof. With the rise of cyber-physical systems in general, and cyber-physical production systems in particular, the interplay between several engineering disciplines, such as software engineering, mechanical engineering and electrical engineering, becomes a must. Thus, a shift from pure software models to system models has to take place to develop the full potential of model-driven engineering for the whole production domain. System models are also essential to raise the level of flexibility of production systems even further in order to better react to changing requirements, since systems are no longer designed to be, but they have to be designed to evolve. In this talk, we will present ongoing work of applying and further developing model-driven techniques, such as consistency management and co-evolution support, for the production domain.

Gerti Kappel

Institute for Software Technology and Interactive Systems at the Vienna University of Technology (Austria)

Tuesday 21 July, 2015
9:00 – 10:30    (plenary session)

Gerti Kappel is a full professor at the Institute for Software Technology and Interactive Systems at the Vienna University of Technology, heading the Business Informatics Group. Until 2001, she was a full professor of computer science and head of the Department of Information Systems at the Johannes Kepler University of Linz. She received the Ms and PhD degrees in computer science and business informatics from the University of Vienna and Vienna University of Technology in 1984 and 1987, respectively. From 1987 to1989 she was a visiting researcher at Centre Universitaire d’Informatique, Geneva, Switzerland.
She has been involved in national and international joint projects, both governmental and industry funded, as well as sponsored by the EU. From 2004 to 2007, she was also dean of student affairs for business informatics.

More details can be found on:


TAP Keynotes

Mind the Gap: At the Crossroads of Design, Implementation, and Foundations

To reduce complexity, general-purpose modeling languages strive for abstraction. But what is the right level of abstraction? Design-oriented models capture the logical or physical organization of software, abstracting from their dynamic behavior. Foundational models capture core features in a way suitable for meta-theory, but rely on cumbersome encodings of other features. Specifications close to actual code get obfuscated by the low-level intricacies of specific implementations.

This talk reports on research on abstract behavioral specifications, aiming for a middle ground in the gap between design, implementation, and foundations. We consider executable, yet abstract models which are faithful to the control and data flow of concurrent and distributed object-oriented systems, yet abstract enough to facilitate formal verification. We then consider how novel technologies such as virtualization and cloud computing reintroduce low-level concerns at the abstraction level of the models. Deployment decisions form an integral part of resource-aware, virtualized applications. We discuss how these technologies raise new challenges for model-based analysis.

Einar Broch Johnsen

University of Oslo (Norway)

Thursday 23 July, 2015
14:00 – 15:30    (plenary session)

Einar Broch Johnsen is Professor at the Department of Informatics, University of Oslo. His research interests are in the field of software development and analysis, spanning from programming languages and methodology, via system specification and modeling, to formal methods and associated theory. Prof. Johnsen is particularly interested in the analysis of concurrent and distributed systems, resource awareness and resource management, and mechanisms for software evolution and reuse. His research in the last years has increasingly focused on abstract behavioral specification formalisms and their use for model-based verification of real systems. Prof. Johnsen is currently coordinating the European research project Engineering Virtualized Services (Envisage) which develops model-based verification techniques to predict the behavior of services deployed on the cloud.

More details can be found on:

Reasoning about C Concurrency and Compilers

The C and C++ languages were originally designed without concurrency support, but the recent revision of the C and C++ standards introduced an intricate but precise semantics for threads; today’s C and C++ compilers, whose optimisers were initially developed in absence of any well-defined concurrency memory model, are being extended to support this new concurrency standard. This is a fantastic opportunity to put at work all our tools to formalise, test, and reason about large scale semantics and software.

In this talk, after recalling the C and C++ memory models, we will explore in a theorem prover the correctness of compiler optimisations and present simple necessary conditions that can be used as a reference by compiler implementers. As an application, we will show how this theory enables building an automatic compiler fuzzer that hunts “concurrency compiler bugs”: subtle wrong code generation bugs which are observable only when the miscompiled functions interact with concurrent contexts.

Perhaps surprisingly, we will also show that by leveraging the semantics of low-level relaxed atomic accesses (which allows programmers to take full advantage of weakly-ordered memory operations), it is possible to build counterexamples to several common source-to-source program transformations (such as expression linearisation and “roach motel” reorderings) that modern compilers perform and that are deemed to be correct. We will evaluate a number of possible local fixes, some strengthening and some weakening the model, and perhaps conclude, that, currently, there is no really satisfactory proposal for the semantics of a general-purpose shared-memory concurrent programming language.

Francesco Zappa Nardelli

INRIA (France)

Friday 24 July, 2015
09:00 – 10:30    (plenary session)

Francesco Zappa Nardelli is a Researcher at Inria Paris – Rocquencourt. His research interests focus on concurrent computation on top of relaxed memory models, ranging from hardware models of modern architectures to high-level programming language specification and compilation. He received his Ph.D. from Université Paris 7 in 2003. Since then, he has worked on language design for distributed computation, type systems for integrating typed and untyped code in scripting languages, and tool support for semantics (including the Ott tool).


More details can be found on:



Testing, fixing, and proving with contracts.

In the mind of the practitioner, the term “formal specification” often conjures up ghastly images of impenetrable logic formulas that only highly-trained experts can digest. Our experience with using contracts indicates, however, that developing simple elements of formal specification embedded in the program text as assertions requires an effort that is generally compatible with standard development practices. In exchange for it, even the very simple contracts that programmers write can improve the effectiveness of a variety of analysis and verification techniques.

In this tutorial, I will present a number of tools we developed for the Eiffel programming language that take advantage of contracts in various guises. AutoTest generates random unit tests and uses contracts as oracles to automatically detect bugs; it has been used to find hundreds of errors in standard libraries. AutoFix builds source-code patches that turn failing tests into passing tests, thus automatically providing program repair for real software faults. AutoProof supports the static full-fledged verification of functional properties in object-oriented software; it has been used to verify the complete functionality of a realistic general-purpose container library. The various tools demonstrate a variety of techniques both dynamic (tests and runtime checking) and static (correctness proofs), which all leverage contracts to improve their effectiveness.

Carlo Alberto Furia

ETH Zurich (Switzerland)

Wednesday 22 July, 2015
14:00 – 15:30

caf-4Carlo A. Furia is a senior researcher at the Chair of Software Engineering in the Department of Computer Science of ETH Zurich. In his research he develops models, techniques, methods, and tools to support the analysis, rigorous development, and verification of software and software-intensive systems. His recent research has focused on improving the applicability and practicality of formal methods by taking advantage of simple program annotations such as contracts and by combining static and dynamic techniques. He is co-chairing SCORE (the student contest on software engineering), an event of ICSE 2016. He has a PhD in Computer Science from the Politecnico di Milano.


More details can be found on: