Program

Monday 18th September

08:15-08:45 REGISTRATION (via Verdi 9)

08:45 – 09:00 Opening Plenary with Paola Pisano, Deputy Mayor for Innovation and Smart City at the City of Torino, Room: Sala Multifunzione 1, via Verdi 9

09:00 – 09:10 FMICS-AVoCS Opening (Laure Petrucci, Cristina Seceleanu), Room: Sala Multifunzione 1 (via Verdi 9)

09:10-10:00 KEYNOTE 1 (chair: Cristina Seceleanu), Room: Sala Multifunzione 1 (via Verdi 9)

Parosh Abdulla, Uppsala University, Sweden
Replacing Store Buffers by Load Buffers in Total Store Ordering

We consider the verification of concurrent programs running under the classical TSO (Total Store Order) memory model. The model allows “write to read” relaxation corresponding to the addition of an unbounded store buffer (that contains pending store operations) between each processor and the main memory. In this talk, we introduce a novel semantics which we call the dual TSO semantics that replaces each store buffer by a load buffer that contains pending load operations. The flow of information is reversed, i.e., store operations are performed by the processes atomically on the main memory, while values of variables are propagated from the memory to the load buffers of the processes. We show that the two semantics are equivalent in the sense that a program will reach identical sets of states when run under the two semantics. Furthermore, we present a simple and effective reachability algorithm for checking safety properties of programs running under the dual semantics.

10:00-10:30 COFFEE BREAK

10:30 – 11:45 SESSION 1 (chair: Cristina Seceleanu): Automated Verification Techniques, Room: Sala Multifunzione 1 (via Verdi 9)

10:30 – 10:55 Dilian Gurov, Christian Lidström, Mattias Nyberg and Jonas Westman: Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report

10:55 – 11:20 Björn Lisper: Verifying Event-Based Timing Constraints by Translation Into Presburger Formulae

11:20 – 11:45 Samuel Huang and Rance Cleaveland: Query Checking for Linear Temporal Logic

12:10 – 13:40 LUNCH

13:40 – 15:20 SESSION 2 (chair: Alessandro Fantechi): Testing and Scheduling, Room: Sala Multifunzione 1 (via Verdi 9)

13:40 – 14:05 Hallan W. Veiga, Max H. Queiroz, Jean-Marie Farines and Marcelo L. Lima: Automatic Conformance Testing of Safety Instrumented Systems for Offshore Oil Platforms

14:05 – 14:30 Alexander Graf-Brill and Holger Hermanns: Model-Based Testing for Asynchronous Systems

14:30 – 14:55 Fabrizio Biondi, Mounir Chadli, Thomas Given-Wilson and Axel Legay: Information Leakage as a Scheduling Resource

14:55 – 15:20 Étienne André: A unified formalism for monoprocessor schedulability analysis under uncertainty

15:20 – 15:50 COFFEE BREAK

19:00 – 22:00 WELCOME RECEPTION at NH Santo Stefano (Area: Quadrilatero Romano, Via Porta Palatina 19)

 

Tuesday 19th September

08:15-09:00 REGISTRATION (via Verdi 9)

09:10-10:00 KEYNOTE 2 (chair: Ana Cavalcanti), Room: Sala Multifunzione 1 (via Verdi 9)

Kerstin Eder, University of Bristol, UK
Towards Formal Apps: Turning formal methods into verification techniques that make a difference in practice

Formal methods offer great potential for increasing the quality of both hardware designs and software systems. While in the hardware domain formal verification techniques have won the trust of verification engineers and designers, much remains to be done to fully exploit the power of formal methods in software development. However, in practice no single technique is adequate to cover a whole system. The key in boosting verification efficiency and system quality is in combining techniques. Widespread acceptance of formal methods requires a clearly expressed usage methodology and a high degree of automation. In hardware verification, formal apps provide solutions that enable non-experts to exhaustively address specific verification challenges which are hard to complete with traditional simulation-based methods. How can we build formal apps for software verification? This presentation is focused on practical techniques for the verification of autonomous systems, with special attention to highlighting where the use of formal methods can significantly increase a developer’s confidence in the correctness of robotic control software from design to implementation. I will draw on examples of popular formal apps used for hardware design verification and discuss the challenges and opportunities we must address including specification, automation, combination of techniques and using AI for verification.

10:00-10:30 COFFEE BREAK

10:30 – 12:10 SESSION 3, SPECIAL TRACK (chair: Ana Cavalcanti): Formal methods for mobile and autonomous robots, Room: Sala Multifunzione 1 (via Verdi 9)

10:30 – 10:55 Paul Gainer, Clare Dixon, Kerstin Dautenhahn, Michael Fisher, Ullrich Hustadt, Joe Saunders and Matt Webster: CRutoN: Automatic Verification of a Robotic Assistant’s Behaviours

10:55 – 11:20 Felipe J. Montana, Jun Liu and Tony J. Dodd: Sampling-based Reactive Motion Planning with Temporal Logic Constraints and Imperfect State Information

11:20 – 11:45 Felipe J. Montana, Jun Liu and Tony J. Dodd: Sampling-based Path Planning for Multi-robot Systems with Co-safe Linear Temporal Logic Specifications

11:45 – 12:10 Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil and Xavier Urbain: Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems

12:10 – 13:40 LUNCH

13:40 – 14:55 SESSION 4 (chair: Laure Petrucci): Modeling and Analysis Techniques, Room: Sala Multifunzione 1 (via Verdi 9)

13:40 – 14:05 Paul Fiterau-Brostean and Falk Howar: Learning Register Automata with Sequence Numbers and Windows of TCP Implementations

14:05 – 14:30 Alessandro Fantechi, Stefania Gnesi and Laura Semini: Optimizing Feature Interaction Detection

14:30 – 14:55 Rutger van Beusekom, Jan Friso Groote, Paul Hoogendijk, Rob Howe, Wieger Wesselink, Rob Wieringa and Tim Willemse: Formalising the Dezyne Modelling Language in mCRL2

15:20 – 15:50 COFFEE BREAK

20:00 – 23:00 SOCIAL DINNER at Ristorante Porto di Savona (Piazza Vittorio Veneto 2)

 

Wednesday 20th September

08:15 – 12:15 TUTORIAL: DIME: Model-based Generation of Running Web applications, Room: Sala Multifunzione 1 (via Verdi 9)

Tutors:

  • Tiziana Margaria, University of Limerick and Lero – The Irish Software Research Centre, Ireland
  • Philip Zweihoff, TU Dortmund, Germany

08:15 – 10:00: Tutorial (first part)

10:00 – 10:30 COFFEE BREAK

10:30 – 12:15 Tutorial (second part)

Brief Description:

DIME is an integrated environment for rigorous model-driven development of web applications that is designed to accelerate the realization of requirements in agile development environments, where change is an essential trait of the application or its environment.
DIME provides a family of Graphical Domain-Specific Languages (GDSLs), each of which is tailored towards a specific aspect of typical web applications. This includes persistent entities (i.e., a data model), business logic in form of various types of process models, the structure of the user interface, and access control. They are modeled on a high level of abstraction in a simplicity-driven fashion that focuses on describing what application is sought, instead of how the application is realized. The choice of platform, programming language, and frameworks is moved to the corresponding (full) code generator.
DIME is itself implemented with the Cinco meta-tooling suite, following a metamodelling based approach.

In this tutorial, we will introduce the principles behind the design of DIME and the choice of the webstack for the runtime, we will illustrate its main capabilities on a simple example and introduce it to the participants in a hands-on session. We will then present and discuss a selection of the applications and other DIME-like systems created with Cinco, with particular attention to security, to configurability, and to the interplay of the different models within an application.