| Monday, November 5th |
|
Room: Olympus |
Room: Hermes |
Room:Athina |
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
|
SMC
(Axel Legay, Kim Larsen)
Introduction
Session 1
|
RSC
(Martin Leucker, César, Sánchez, Gerardo Schneider )
Introduction
Session 1
|
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 |
Introduction to SMC: past present and future
Axel Legay, Kim Larsen
Chasing Errors using Biasing Automata
Doron Peled, Lei Bu, Dachuan Shen, Yael Tzirulnikov
|
Smart Contracts and Opportunities to Formal Methods
Andrew Miller, Zhicheng Cai, Somesh Jha
Contracts over Smart Contracts: Recovering from Violations Dynamically
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
|
SMC
Session 2: On reducing the number of simulations
|
RSC
Session 2
|
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 |
On the Sequential Massart Algorithm for Statistical Model Checking
Cyille Jegourel, Jun Sun, Jin-Song Dong
Quantitative risk assessment of safety-critical Systems via guided simulation for rare events
Stefan Puch, Martin Fraenzle, Sebastian Gerwinn |
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: Modeling as Programming
|
SMC
Session 3: On handling extended models
|
RSC
Session 3
|
Programming is Modeling
Rance Cleaveland
Programming Language Specification and Implementation
Peter Sestoft
Modeling with Scala
Klaus Havelund, Rajeev Joshi
This Is Not A Model
Ole Lehrmann Madsen, Birger Möller-Pedersen |
Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes
Pranav Ashok, Tomas Brazdil, Jan Kretinsky, Ondrej Slamecka
Lightweight Statistical Model Checking in Nondeterministic Continuous Time
Pedro D’Argenio, Arnd Hartmanns, Sean Sedwards
Statistical Model-Checking of Incomplete Stochastic Systems
Shiraj Arora, Louis-Marie Traonouez, Axel Legay, Tania Richmond |
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
|
ETSV
(Markus Schordan, Dirk Beyer, Stephen F. Siegel)
Session 1: Strategy Selection and Combination of Approaches
Introduction
|
RSC
Session 4
|
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
From Computational Thinking to Constructive Design with Simple Models
Tiziana Margaria |
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 |
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 |
|
19:00 |
Welcome Reception |
| Tuesday, November 6th |
|
Room: tba |
Room: tba |
Room:tba |
9:00 |
UVMP
Session 5: Tailoring Languages
|
ETSV
Session 2: Verification Tool Performance
|
SMC
Session 4: Applications
|
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
On the Difficulty of Drawing the Line
Steve Bosselmann, Stefan Naujokat, Bernhard Steffen |
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 |
Statistical Model Checking a Moving Block Railway Signalling Scenario with Uppaal SMC
Maurice ter Beek, Davide Basile, Vincenzo Ciancia
Mitigating Security Risks through Attack Strategies Exploration
Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Axel Legay, Saddek
Bensalem
Statistical Model Checking of Processor Systems in Various Interrupt Scenarios
Josef Strnadel |
|
|
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: Olympus |
Room: Hermes |
Room:Athina |
9:00 |
FMIP
(Michael Felderer, Dilian Gurov, Marieke Huisman, Björn Lisper, Rupert Schlick)
Introduction
Session 1: Testing and requirements in Industrial practice
|
RV
(Ezio Bartocci, Ylies Falcone)
Introduction
Session 1: Monitoring Cyber-Physical Systems and the Internet of Things
|
REoCAS
(Rocco De Nicola, Stefan Jähnichen, Martin Wirsing)
Introduction
Session 1: Formal Modelling of Collective Adaptive Systems
DReAM. |
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. |
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 |
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
|
RV
Session 2: RV for Industrial and Large-scale Systems
|
REoCAS
Session 2: Engineering Collective Adaptive Systems
|
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 |
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 |
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
|
RV
Session 3: Latest Advances on Software Monitoring
|
REoCAS
Session 3: Panel
|
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 |
BDDs on the run
K. Havelund, D. Peled
Verifying real-world software with contracts for concurrency
J.M. Lourenco |
The Meaning of Adaptation: Mastering the Unforeseen?
Martin Wirsing, Stefan Jaehnichen, Rocco De Nicola |
|
Discussion |
Discussion |
Discussion |
15:30 |
COFFEE BREAK |
16:00 |
FMIP
Session 4: A Repository of Formal Methods Benchmarks
|
DocSym
(Anna-Lena Lamprecht)
|
FoMaC
Meeting of the Editorial Board |
A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods
Schlick et al. |
Industry 4.0 – A Threat or Opportunity?
Barbara Steffen
Continuous Practices in the Context of Model-Driven System Development
Tim Tegeler
Enabling Automated Compliance Checking of Processes against Safety Standards
Julieth Patricia Castellanos Ardila
Assuring Intelligent Ambient Assisted Living Solutions by Statistical Model Checking
Ashalatha Kunnappilly, Raluca Marinescu and Cristina Seceleanu
Implementation of Privacy Calculus and its Type Checking in Maude
Georgios Pitsiladis and Petros Stefaneas
Model Checking of Procedural Systems
Alnis Murtowi |
|
|
Discussion |
|
Discussion |
| Thursday, November 8th |
|
Room: Olympus |
Room:Hermes |
Room:Athina |
9:00 |
XbyC
(Maurice H. ter Beek, Loek Cleophas, Ina Schaefer, Bruce W. Watson)
Introduction
|
VVDS
(Christina Seceleanu)
Introduction
Session 1: Verification of Distributed Algorithms and Concurrent Programs
|
REoCAS
Session 4: Testing and Safety of Collective Adaptive Systems
|
X-by Construction
Maurice ter Beek, Loek Cloephas, Ina Schaefer, Bruce Watson
Session 1
(Some) Security by Construction through a LangSec Approach
Erik Poll |
ByMC-Byzantine Model Checker
Igor Konnov, Josef Widder
Statid code verification through process models
Sebastiaan Joosten, Marieke Huisman |
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
|
VVDS
Session 2: Testing Distributed Transactions, IoT and Cyber-Physical Systems
|
REoCAS
Session 5: Security and Performance of Collective Adaptive Systems
|
Program Correctness by Transformation
Marieke Huisman
Design 4 X through Model Transformation
Bernhard Steffen
Modelling by Patterns for Correct-by-Construction Process
Dominique Méry |
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 |
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
|
RERS
(Bernhard Steffen)
Introduction
Session 1 RERS Challenge
|
REoCAS
Session 6: Machine Learning and Evolutionary Computing for Collective Adaptive Systems
|
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 2018 overview, scored achievements and ranking
Bernhard Steffen
Approaches and results
presentations by participants |
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
|
RERS
Session 2 RERS Challenge
|
REoCAS
Session 7: Software Support and Case Studies
|
Is Privacy by Construction Possible?
Gerardo Schneider
X-by-X: Non-Functional Security
Axel Legay
Towards Confidentiality-by-Construction
Ina Schaefer |
Approaches and results
presentations by participants |
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 |
End of sessions |
| Friday, November 9th |
|
Room:Olympus |
Room:Hermes |
Room:Athina |
9:00 |
ABVOV
(Wolfgang Ahrendt, Marieke Huisman, Giles Reger, Kristin Yvonne Rozier)
Introduction
Session 1
What are the relevant Program Properties?
|
CPS
(J. Paul Gibson, Marc Pantel, Peter Gorm Larsen, Jim Woodcock, John Fitzgerald)
Introduction
Session 1 | <
Industrial Day
Session 1
Digitalisation and Industry 4.0 |
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
Towards a Notion of Coverage for Incomplete Program-Correctness Proofs
Bernhard Beckert, Stefan Kobischke, Mattias Ulbrich, Mihai Herda |
Cyber-Physical Systems Engineering: An Introduction
Paul Gibson, Peter Gorm Larsen, Marc Pantel, John Fitzgerald, James
Woodcock
Intelligent Adaption Process in Cyber-Physical Production Systems (CPPS)
Daniel Mueller, Christin Schumacher, Felix Zeidler
Model-Based Systems Engineering for Systems Simulation
Renan Leroux-Beaudout, Marc Pantel, Ileana Ober, Jean-Michel Bruel
Scenario-based validation of automated driving Systems
Hardi Hungar |
GOLD: Global Organization aLignment and Decision - Towards the Hierarchical Integration of Heterogeneous Business Models.
Barbara Steffen and Steve Bosselmann
A Methodology for Combinatory Process Synthesis: Process Variability in Clinical Pathways.
Tristan Schäfer, Frederik Möller, Anja Burmann, Yevgen Pikus, Norbert Weißenberg, Marcus Hintze, Jakob Rehof
Automatic composition of rough solution possibilities in the target planning of factory planning projects by means of combinatory logic.
Jan Winkels, Julian Graefenstein, Tristan Schäfer, David Scholz, Jakob Rehof, Michael Henke |
|
Discussion |
Discussion |
Discussion |
10:30 |
COFFEE BREAK |
11:00 |
ABVOV
Session 2
Putting Combinations of Static and Runtime Verification Into Practice
|
CPS
Session 2
|
Industrial Day
Session 2
Machine Learning in Automotive Systems |
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 |
Engineering of Cyber-Physical Systems in the automotive context: case study of a range prediction assistant
Christian Koenig, Gerd Meisl, Natalia Balcu, Benjamin Vosseler, Henrik
Hörmann, Jos Höll, Victor Fäßler
Testing Avionics Software: Is FMI up to the Task?
Jörg Brauer, Jan Peleska, Oliver Möller
Lessons Learned Using FMI Co-Simulation for Model-based Design of Cyber Physical Systems
Luis Diogo Couto, Stylianos Basagiannis, El Hassan Ridouane, Erica
Zavaglio, Pasquale Antonante, Hajer Saada, Sara Falleni
Co-simulation: the Past, Future, and Open Challenges
Cláudio Gomes, Casper Thule, Julien Deantoni, Peter Gorm Larsen, Hans Vangheluwe |
Applicability of Neuronal Networks for Driving Style Classification and Maneuver Detection.
Karl-Falco Storm, Paul Hochrein, Peter Engel, Anderas Rausch
Drivable region detection using Deep Neural Network.
Ishwarya Chandrasekaran, Marwan Sabih, Andreas Rausch |
|
Discussion |
Discussion |
Discussion |
12.30 |
LUNCH |
14:00 |
ABVOV
Session 3
Application Areas for combining Static and Runtime Verification
|
CPS
Session 3
Discussion and position paper draft |
Industrial Day
Session 3
RV tools of industrial strength and/or challenges for runtime verification from industrial partners - Joint with COST ARVI |
Programming Safe Robotics Systems: Challenges and Advances
Ankush Desai, Shaz Qadeer, Sanjit Seshia
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 |
|
Industrial RV Tool Demo, Runtime Verification Inc.
Grigore Rosu
RV demo in industrial financial transaction systems, collaboration with Ixaris Ltd.
Shaun Azzopardi and Christian Colombo |
|
Discussion |
Discussion |
Discussion |
15:30 |
Coffee Break |
16:00 |
DocSym
|
INTO-CPS
General Assembly |
Industrial Day
Session 4
EU-Project Workshops - Joint with COST ARVI |
Architectures for Constraint Management
Malte Mues
Implementing Efficient Workflow Synthesis Algorithms Using SAT Solving Techniques
Vedran Kasalica
Annotated Models in Model-based Compilations
Steven Smyth, Alexander Schulz-Rosengarten and Reinhard von Hanxleden
Model-Based Code Generators for Domain Specific Tools
Michael Lybecait
Holistic DSL Web Modeling
Philip Zweihoff
Learning-Based Testing in Practice
Alexander Bainczyk |
The General Assembly 2018 for the INTO-CPS Association |
Elastest - An elastic platform to ease end to end testing
Cesar Sanchez
COEMS - Continuous Observation of Embedded Multicore Systems
Martin Leucker |
17:30 |
End of Sessions |
