Programme

ISoLA Tracks Schedule


Monday
Nov 05



Tuesday
Nov 06



Wednesday
Nov 07



Thursday
Nov 08



Friday
Nov 09


UVMP SMC RSC UVMP ETSV SMC FMIP RV REoCAS XbyC VVDS REoCAS ABVOV C-PSE Ind Day
UVMP SMC RSC UVMP ETSV   FMIP RV REoCAS XbyC VVDS REoCAS ABVOV C-PSE Ind Day
UVMP SMC RSC Outing     FMIP RV REoCAS XbyC RERS REoCAS ABVOV C-PSE Ind Day
UVMP ETSV RSC Outing     FMIP DocSymp FoMaC XbyC RERS REoCAS DocSymp   Ind Day

Sunday, November 4th

 

Room: tba

14:00 -18:00

Welcome Reception and Registration

20:00

 

 

Monday, November 5th

 

Room: tba

Room: tba

Room:tba

8:00

Registration

8:45

Opening ISoLA

9:00

UVMP
(Manfred Broy, Klaus Havelund, Rahul Kumar, Bernhard Steffen)
Introduction
Session 1: On Modeling and Programming
On Modeling and Programming
Neil Jones
Definition of Modeling vs. Programming Languages
Maged Elaasar
A Non-unified View of Modelling, Specification and Programming
Stefan Hallerstede, Peter Gorm Larsen, John Fitzgerald
Using Umple to Synergistically Process Features, Variants, UML Models and Classic Code
Timothy Lethbridge, Abdulaziz Algablan

SMC
(Axel Legay, Kim Larsen)

Introduction
Session 1
Introduction to SMC: past present and future
Axel Legay, Kim Larsen
Talk: Chasing Errors using Biasing Automata

RSC
(Martin Leucker, César, Sánchez, Gerardo Schneider )

Introduction
Session 1:
Smart Contracts and Opportunities to Formal Methods
Andrew Miller, Zhicheng Cai, Somesh Jha
Contracts over Smart Contracts: Recovering from Violations Dynamically Track
Gordon Pace, Christian Colombo, Joshua Ellul
Security Analysis of Smart Contracts in Datalog
Peter Tsankov

 

Discussion

Discussion

Discussion

10:30

COFFEE BREAK

11:00

UVMP
Session 2: Formal Methods and Proofs
Why programming must be supported by modeling and how?
Egon Boerger
On Models and Code-A Unified Approach to Support Large-Scale Deductive Program Verification
Marieke Huisman
Type Theory as a Framework for Modelling and Programming
Cezar Ionescu, Patrik Jansson, Nicola Botta
Bringing Effortless Refinement of Data Layouts to Cogent
Liam O´Connor, Zilin Chen, Partha Susarla, Gerwin Klein, Christine Rizkallah, Gabriele Keller

SMC
Session 2: On reducing the number of simulations
On the Sequential Massart Algorithm for Statistical Model Checking

Quantitative risk assessment of safety-critical Systems via guided simulation for rare events

RSC
Session 2

Temporal Properties of Smart Contracts
Ilya Sergey, Amnit Kumar, Aquinas Hobor
Temporal Aspects of Smart Contracts for Financial Derivatives
Christopher Clack, Gabriel Vanca
Marlowe: financial contracts on blockchain
Simon Thompson, Pablo Lamela Seljas

 

Discussion

Discussion

Discussion

12:30

LUNCH

14:00

UVMP
Session 3: Programming as Modeling

Programming is Modeling
Rance Cleaveland
Programming language specification and implementation
Peter Sestoft
Modeling with Scala
Klaus Havelund
This is not a model
Birger Möller-Pedersen, Ole Lehrmann Madsen

SMC
Session 3: On handling extended models

Monte Carlo Tree Search   for Verifying Reachability in Markov Decision Processes

Lightweight Statistical Model Checking in Nondeterministic Continuous Time

Statistical Model-Checking of Incomplete Stochastic Systems

RSC
Session 3

SMT-based Verification of Solidity Smart Contracts
Leonardo Alt, Christian Reitwiessner
Blockchains as Kripke Models: an Analysis of Atomic Cross-Chain Swap
Yoichi Hirai
A Language-Independent Approach To Smart Contracts Verification
Xiaochong Chen, Daejun Park, Grigore Rosu

 

Discussion

Discussion

Discussion

15:30

COFFEE BREAK

16:00

UVMP
Session 4: “The Application Perspective” or “Pragmatics”

A Unified Approach for Modeling, Developing, and Assuring Critical Systems
Brian Larson, John Hatcliff, Robby, Jason Belt, Yi Zhang
Towards Interactive Compilation Models
Steven Smyth, Alexander Schulz-Rosengarten, Reinhard von Hanxleden
Computation Thinking…
Tiziana Margaria

ETSV
(Markus Schordan, Dirk Beyer, Stephen F. Siegel)
Session 1: Strategy Selection and Combination of Approaches
Introduction
Strategy Selection for Software Verification Based on Boolean Features: A Simple but Effective Approach
Dirk Beyer, Matthias Dangl
Symbolic Execution and Deductive Verification Approaches to VerifyThis 2017 Challenges
Ziqing Luo, Stephen F. Siegel

RSC
Session 4

Towards Adding Variety to Simplicity
Nachiappan Valliappan, Solène Mirliaz, Elisabet Lobo Vesga, Alejandro Rosso
Fun with Bitcoin smart contracts
Massimo Bartoletti, Roberto Zunino, Tiziana Cimoli
Computing Exact Worst-Case Gas Consumption to Smart Contracts
Matteo Marescotti, Martin Blicha, Anti Hyvarinen, Sepideh Asadi, Natasha Sharygina

 

Discussion

Discussion

Discussion

17:30

 



Tuesday, November 6th

 

Room: tba

Room: tba

Room:tba

9:00

UVMP
Session 5: Tailoring Languages

Design Languages: A Necessary New Generation of Computer Languages
Bran Selic
From Modeling to Model-based Programming
Gabor Karsai
Fusing Modeling and Programming into Language-Oriented Programming
Markus Voelter
Language-Oriented Software Development
Bernhard Steffen

ETSV
Session 2: Verification Tool Performance

Runtime and Memory Evaluation of Data Race Detection Tools
Pei-Hung Lin, Chunhua Liao, Markus Schordan, Ian Karlin
In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching
Dirk Beyer, Karlheinz Friedberger
Discussion: (1) Cooperative Verification, (2) Deductive vs. finite-state verification

SMC
Session 4: Applications

Statistical Model Checking a Moving Block Railway Signalling Scenario with Uppaal SMC

Mitigating Security Risks through Attack Strategies Exploration

Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

 

Discussion

Discussion

Discussion

10:30

COFFEE BREAK

11:00

UVMP
Session 6 Panel Session

ETSV
Session 3: Verification of Real-World
Programs vs. Artificial Benchmarks
Deductive Verification of Unmodified Linux Kernel Library Functions
Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov
Synthesizing Subtle Bugs with Known Witnesses
Marc Jasper, Bernhard Steffen
Discussion: (1) Dynamic vs. static verification tools, (2) Verification competitions

 

 

Discussion

Discussion

Discussion

12:30

LUNCH

14:30
22:00

 

Excursion and Conference Dinner

 

Wednesday, November 7th

 

Room: tba

Room: tba

Room:tba

9:00

FMIP
(Michael Felderer, Dilian Gurov, Marieke Huisman, Björn Lisper, Rupert Schlick)
Introduction
Session 1: Testing and requirements in Industrial practice
Model-based Testing for Avionic Systems Proven Benefits and Further Challenges
Peleska et al.
Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process
Bardin et al.
Pitfalls upon Applying Model learning to Industrial Legacy Software
Alzuhaibi et al.

RV
(Ezio Bartocci, Ylies Falcone)

Introduction
Session 1: Monitoring Cyber-Physical Systems and the Internet of Things
Opportunities and challenges in monitoring cyber-physical systems security
B. Bonakdarpour, J. Deshmukh, M. Pajic
Migrating monitors + ABE: A suitable combination for secure IoT?
G. Pace, P. Picazo-Sanchez, G. Schneider
Capturing Inter-process communication for run-time verification on Android
A.Villazon, H. Sun, W. Binder

REoCAS
(Rocco De Nicola, Stefan Jähnichen, Martin Wirsing)

Introduction
Session 1: Formal Modelling of Collective Adaptive Systems
DReAM. Dynamic Reconfigurable Architecture Modeling
Alessandro Maggi, Joseph Sifakis, Rocco De Nicola
Dynamic Logic for Ensembles
Rolf Hennicker, Martin Wirsing
Modelling the Transition to Distributed Ledgers
Jan Sürmeli, Stefan Jähnichen, J. W. Sanders

 

Discussion

Discussion

Discussion

10:30

COFFEE BREAK

11:00

FMIP
Session 2: Software Verification in Industrial Practice

Formal Verification in Automotive Industry: Enablers and Obstacles
Nyberg et al.
Scalability of Deductive Verification Depends on Method Call Treatment
Knüppel et al.
Java Automated Deductive Verification in Practice: Lessons from industrial proof-based projects
Cok

RV
Session 2: RV for Industrial and Large-scale Systems

Considering academia-Industry projects meta-characteristics in runtime verification design
C. Colombo, G. Pace
Flexible monitor deployment for runtime verification of large scale software
T. Zhang, G. Eakman, O. Sokolsky, I. Lee
Increasing the reusability of enforcers with lifecycle events
O. Riganelli, D. Micucci, L. Mariani

REoCAS
Session 2: Engineering Collective Adaptive Systems

A Collective Adaptive Socio-Technical System for Remote- and Self-Supervised Exercise in the Treatment of Intermittent Claudication
Jeremy Pitt, Kristina Milanovic, Alexander Coupland, Tim Allan, Alun Davies, Tristan Lane, Anna Maria Malagoni, Ankur Thapar, Joseph Shalhoub
Engineering Collectives of Self-driving Vehicles: the SOTA Approach
Dhaminda Abeywickrama, Marco Mamei, Franco Zambonelli
Synthesizing Capabilities for Collective Adaptive Systems for Self-Descriptive Hardware Devices – Bridging the Reality Gap
Constantin Wanninger, Christian Eymüller, Alwin Hoffmann, Oliver Kosak, Wolfgang Reif

 

Discussion

Discussion

Discussion

12:30

LUNCH

14:00

FMIP
Session 3: Application Areas

Security Filters for IoT Domain Isolation
Bolignano and Plateau
20 Years of Uppaal Enabled Industrial Model-Based Validation and Beyond
Larsen et al.
Verification of Operating System Monolithic Kernels without Extensions
Zakharov and Novikov

RV
Session 3: Latest Advances on Software Monitoring

BDDs on the run
K. Havelund, D. Peled
Verifying real-world software with contracts for concurrency
J.M. Lourenco

REoCAS
Session 3: Panel

The Meaning of Adaptation
Stefan Jähnichen (Moderator), Tomas Bures, NN, NN, Jeremy Pitt, Franco Zambonelli

 

Discussion

Discussion

Discussion

15:30

COFFEE BREAK

16:00

FMIP
Session 4: A Repository of Formal Methods Benchmarks

A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods
Schlick et al.

DocSym
(Anna-Lena Lamprecht)

  • * Barbara Steffen (Rotterdam School of Management, Netherlands): Industry 4.0 – A Threat or Opportunity?
  • * Tim Tegeler (TU Dortmund, Germany): Continuous Practices in the Context of Model-Driven System Development
  • * Julieth Patricia Castellanos Ardila (Mälardalen University, Sweden): Enabling Automated Compliance Checking of Processes against Safety Standards
  • * Ashalatha Kunnappilly, Raluca Marinescu and Cristina Seceleanu (Mälardalen University, Sweden): Assuring Intelligent Ambient Assisted Living Solutions by Statistical Model Checking
  • * Georgios Pitsiladis and Petros Stefaneas (National and Kapodistrian University of Athens and National Technical University of Athens, Greece): Implementation of Privacy Calculus and its Type Checking in Maude
  • * Alnis Murtowi (TU Dortmund, Germany): Model Checking of Procedural Systems

 

FoMaC
Meeting of the Editorial Board

 

Discussion

 

Discussion

17:30

18:00

Optional Excursion and Fish Dinner



Thursday, November 8th

 

Room: tba

Room: tba

Room:tba

9:00

XbyC
(Maurice H. ter Beek, Loek Cleophas, Ina Schaefer, Bruce W. Watson)

Introduction
X-by Construction
Maurice ter Beek, Loek Cloephas, Ina Schaefer, Bruce Watson
Session 1
(Some) Security by Construction through a LangSec Approach
Erik Poll

VVDS
(Christina Seceleanu)

Introduction
Session 1: Verification of Distributed Algorithms and Concurrent Programs
ByMC-Byzantine Model Checker
Igor Konnov, Josef Widder
Statid code verification through process models
Sebastiaan Joosten, Marieke Huisman

REoCAS
Session 4: Testing and Safety of Collective Adaptive Systems

Mutation-based Test Suite Evolution for Self-Organizing Systems
André Reichstaller, Thomas Gabor, Alexander Knapp
Adapting Quality Assurance to Adaptive Systems: The Scenario Coevolution Paradigm
Thomas Gabor, Marie Kiermeier, Andreas Sedlmeier, Bernhard Kempter, Cornel Klein, Horst Sauer, Reiner Schmid, Jan Wieghardt
Designing Systems with Detection and Reconfiguration Capabilities: A Formal Approach
Iulia Dragomir, Simon Iosti, Marius Bozga, Saddek Bensalem

 

Discussion

Discussion

Discussion

10:30

COFFEE BREAK

11:00

XbyC
Session 2
Program Correctness by Transformatio
n
Marieke Huisman
Design 4 X through Model Transformation
Bernhard Steffen
Modelling by Patterns for Correct-by-Construction Process
Dominique Méry

VVDS
Session 2: Testing Distributed Transactions, IoT and Cyber-Physical Systems

Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems
Simin Cai, Barbara Gallina, Dag Nyström, Cristina Sceleanu
Towards automated testing of the Internet of Things: Results obtained with the TESTAR tool
Mirella Martinez, Anna Isabel Esparcia-Alcazar, Tanja E.J. Vos, Pekka Aho, Joan Fons i Cors
Quantitative Safety Analysis of a Coordinated Emergency Brake Protocol for Vehicle Platoons
Carl Bergenhem, Karl Meinke, Fabian Ström

REoCAS
Session 5: Security and Performance of Collective Adaptive Systems

Dynamic Security Specification through Autonomic Component Ensembles
Rima Al Ali, Tomas Bures, Petr Hnetynka, Filip Krijt, Frantisek Plasil, Jiri Vinarek
Differential Equivalence yields Network Centrality
Stefano Tognazzi, Mirco Tribastone, Max Tschaikowski, Andrea Vandin
Measuring and Evaluating the Performance of Self-Organization Mechanisms within Collective Adaptive Systems
Benedikt Eberhardinger, Hella Ponsar, Dominik Klumpp, Wolfgang Reif

 

Discussion

Discussion

Discussion

12.30

LUNCH

14:00

XbyC
Session 3

Modular, Correct Compilation with Automatic Soundness Proofs
Reiner Hähnle
Deployment by Construction for Multicore Architectures
Einar Broch Johnsen
Towards Software Performance by Construction
Mirco Tribastone

RERS
(Bernhard Steffen)

Introduction
Session 1 RERS Challenge
RERS 2018 overview, scored achievements and ranking
Bernhard Steffen
Approaches and results
presentations  by participants

REoCAS
Session 6: Machine Learning and Evolutionary Computing for Collective Adaptive Systems

Engineering Sustainable and Adaptive Systems in Dynamic and Unpredictable Environments
Rui P. Cardoso, Rosaldo J.F. Rossetti, Emma Hart, David Burth Kurka, Jeremy Pitt
The Sharer´s Dilemma in Collective Adaptive Systems of Self-Interested Agents
Lenz Belzner, Kyrill Schmid, Thomy Phan, Thomas Gabor, Martin Wirsing
Coordination model with reinforcement learning for ensuring reliable on-demand services in collective adaptive systems
Houssem Ben Mahfoudh, Giovanna Di Marzo Serugendo, Anthony Boulmier, Nabil Abdennadher

 

Discussion

Discussion

Discussion

15:30

Coffee Break

16:00

XbyC
Session 4

Is Privacy by Construction Possible?
Gerardo Schneider
X-by-X: Non-Functional Security
Axel Legay
Towards Confidentiality-by-Construction
Ina Schaefer

RERS
Session 2 RERS Challenge

Approaches and results
presentations by participants

REoCAS
Session 7: Software Support and Case Studies

Data-driven modelling and simulation of urban transportation systems using Carma
Natalia Zon, Stephen Gilmore
GoAt: Attribute-based Interaction in Google Go
Yehia Abd Alrahman, Rocco De Nicola, Giulio Garbi
Four Exercises in Programming Dynamic Reconfigurable Systems: Methodology and Solution in DR-BIP
Rim El Ballouli, Saddek Bensalem, Marius Bozga, Joseph Sifakis

 

Discussion

Discussion

Discussion

 

17:30

 

 

<
Friday, November 9th

 

Room: tba

Room: tba

Room:tba

9:00

ABVOV
(Wolfgang Ahrendt, Marieke Huisman, Giles Reger, Kristin Yvonne Rozier)

Introduction
Session 1: What are the relevant Program Properties?
Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification
Borzoo Bonakdarpour, César Sánchez, Gerardo Schneider
Temporal Reasoning on Incomplete Paths
Dana Fisman, Hillel Kugler
A Framework for Quantitative Assessment of Partial Program Correctness Proofs
Bernhard Beckert, Mihai Herda, Stefan Kobischke, Mattias Ulbrich

CPS
(J. Paul Gibson, Marc Pantel, Peter Gorm Larsen, Jim Woodcock, John Fitzgerald)

Introduction
Cyber-Physical Systems Engineering: An Introduction
Session 1
Intelligent Adaption Process in Cyber-Physical Production Systems

Model-Based Systems Engineering for Systems Simulation

Scenario-based validation of automated driving Systems

Industrial Day
(Falk Howar)

 

Discussion

Discussion

Discussion

10:30

COFFEE BREAK

11:00

ABVOV
Session 2: Putting Combinations of Static and Runtime Verification Into Practice

Generating Inductive Shape Predicates for Runtime Checking and Formal Verification
Jan H. Boockmann, Gerald Lüttgen, Jan Tobias Mühlberg
Runtime Assertion Checking and Static Verification: Collaborative Partners
Fonenantsoa Maurica, David Cok, Julien Signoles
A Language-Independent Program Verification Framework
Xiahong Chen, Grigore Rosu

CPS
Session 2
Engineering of Cyber-Physical
Systems in the automotive context: case study of a range prediction assistant

Testing Avionics Software: Is FMI up to the Task?

Lessons Learned Using FMI Co-Simulation for Model-based Design of Cyber Physical Systems

Co-simulation: the Past, Future, and Open Challenges

Industrial Day

 

Discussion

Discussion

Discussion

12.30

LUNCH

14:00

ABVOV
Session 3: Application Areas for combining Static and Runtime Verification

Programming Safe Robotics Systems: Challenges, Advances, and Opportunities
Ankush Desai, Sanjit Seshia, Shaz Qadeer
Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring
Falk Howar, Dimitra Giannakopoulou, Malte Mues, Jorge Navas
Panel discussion on future steps on combining runtime and static verification

CPS
Session 3

Discussion and position paper draft

Industrial Day

 

Discussion

Discussion

Discussion

15:30

Coffee Break

16:00

DocSym

  • * Malte Mues (TU Dortmund, Germany): Architectures for Constraint Management
  • * Vedran Kasalica (Utrecht University, Netherlands): Implementing Efficient Workflow Synthesis Algorithms Using SAT Solving Techniques
  • * Steven Smyth, Alexander Schulz-Rosengarten and Reinhard von Hanxleden (Kiel University, Germany): Annotated Models in Model-based Compilations
  • * Michael Lybecait (TU Dortmund, Germany): Model-Based Code Generators for Domain Specific Tools
  • * Philip Zweihoff (TU Dortmund, Germany): Holistic DSL Web Modeling
  • * Alexander Bainczyk (TU Dortmund, Germany): Learning-Based Testing in Practice

 

 

Industrial Day

17:30

 



Co-Sponsored By
Other Sponsors