Program

Proceedings

The proceedings are available. Find information about the print edition and the on-line edition .

Bus Transfer

A bus transfer has been organized for Sunday morning. The bus leaves at 8:00 at Hotel Cabin and will pick you up at Hlemmur, Lækjartorg and BSÍ station.

Program Overview

A PDF version of the programme is available.

Wednesday, June 1

 8:45- 9:00 Opening

Room M101, Marjan Sirjani

 9:00-10:00 Invited talk 1

Room M101, Chair: Erika Abraham

Reiner Hähnle.
Can Formal Methods Improve the Efficiency of Code Reviews?

10:30-12:00 Session 1: Program verification

Room M101, Chair: Gerardo Schneider

Ferruccio Damiani and Michael Lienhardt.
On Type Checking Delta-Oriented Product Lines

Leo Freitas, James Baxter, Ana Cavalcanti and Andy Wellings.
Verifying a priority scheduler for an SCJ runtime environment

Michael Ameri and Carlo A. Furia. Why Just Boogie?
Translating Between Intermediate Verification Languages

10:30-12:00 Session 2: Probabilistic systems

Room V102, Chair: John Derrick

Sean Sedwards, Pedro D'Argenio, Arnd Hartmanns and Axel Legay.
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata

Oana Andrei, Muffy Calder, Matthew Chalmers, Alistair Morrison and Mattias Rost.
Probabilistic Formal Analysis of App Usage to Inform Redesign

Lubos Korenciak, Vojtech Rehak and Adrian Farmadin.
Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-delay CTMC

13:30-15:00 Session 3: Concurrency I

Room M101, Chair: Heike Wehrheim

Hosein Nazarpour, Ylies Falcone, Saddek Bensalem, Marius Bozga and Jacques Combaz.
Monitoring Multi-threaded Component-Based Systems

Sascha Fendrich and Gerald Luettgen.
A Generalised Theory of Interface Automata, Component Compatibility and Error

Ian Cassar and Adrian Francalanza.
On Implementing a Monitor-Oriented Programming Framework for Actor Systems

15:30-17:00 Session 4: Concurrency II (Room M101)

Room M101, Chair: Ferruccio Damiani

Gerhard Schellhorn, Oleg Travkin and Heike Wehrheim.
Towards a Thread-Local Proof Technique for Starvation Freedom

Olaf Owe.
Reasoning about Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems

Matt Luckcuck, Ana Cavaltanti and Andy Wellings.
A Formal Model of the Safety-Critical Java Level 2 Paradigm

17:15-18:45 Reception

Nauthóll

18:15-19:00 Steering Committee Meeting

Room V102

Thursday, June 2

9:00-10:00 Invited talk 2

Room M101, Chair: Marieke Huisman

Marsha Chechik.
Dimensions of Model Transformation Reuse

10:30-12:00 Session 5: Safety and liveness

Room: M101, Chair: Einar Broch Johnsen

Stephan Barth.
Deciding Monadic Second Order Logic over omega-words by Specialized Finite Automata

Christian Prehofer.
Property Preservation for Extension Patterns of State Transition Diagrams

Jens Bendisposto, Philipp Koerner, Michael Leuschel, Jeroen Meijer, Jaco Van de Pol, Helen Treharne and Jorden Whitefield.
Symbolic Reachability Analysis of B through ProB and LTSmin

10:30-12:00 Session 6: Model learning

Room V102, Chair: Reiner Hähnle

Petra van den Bos, Rick Smetsers and Frits Vaandrager.
Enhancing Automata Learning by Log-Based Metrics

Mathijs Schuts, Jozef Hooman and Frits Vaandrager.
Refactoring of Legacy Software using Model Learning and Equivalence Checking: An Industrial Experience Report

Wei Chen, David Aspinall, Andrew D. Gordon, Charles Sutton and Igor Muttik.
On Robust Malware Classifiers by Verifying Unwanted Behaviours

13:30-18:30 Excursion

Participants of the Reykjavik Erupts (June 2) excursion will be picked up at 13:30.

See this page for other suggestions.

19:30 Conference Dinner

Kolabrautin

Friday June 3

9:00-10:00 Invited talk 3

Room M101, Chair: Marjan Sirjani

Laura Kovács.
Symbolic Computation and Automated Reasoning for Program Analysis

10:30-12:00 Session 7: SAT and SMT solving

Room: M101, Chair: Cesar Sanchez

Pedro Antonino, Bill Roscoe and Thomas Gibson-Robinson.
Efficient Deadlock Checking using Local Analysis and SAT Solving

Sebastian Krings and Michael Leuschel.
SMT Solvers for Validation of B and Event-B models

Andrii Kovalov and Juliana Küster Filipe Bowles.
Avoiding Medication Conflicts for Patients with Multimorbidities

10:30-12:00 Session 8: Testing

Room: V102, Chair: Wolfgang Ahrendt

Adrian Riesco and Juan Rodriguez-Hortala.
Temporal Random Testing for Spark Streaming

Elvira Albert, Miguel Gomez-Zamalloa and Miguel Isabel.
Combining Static Analysis and Testing for Deadlock Detection

Renáta Hodován and Akos Kiss.
Fuzzing JavaScript Engine APIs

13:30-15:00 Session 9: Theorem proving and constraint satisfaction

Room: M101, Chair: Laura Kovacs

Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
A Component-based Approach to Hybrid Systems Safety Verification

Viorel Preoteasa.
Verifying Pointer Programs using Separation Logic and Invariant Based Programming in Isabelle

Pavel Zaichenkov, Olga Tveretina and Alex Shafarenko.
A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces

15:30-17:00 Session 10: Case studies

Room: M101, Chair: Marcel Kyas

Bjørnar Luteberget, Christian Johansen and Martin Steffen.
Rule-based Consistency Checking of Railway Infrastructure Designs

Dániel Darvas, István Majzik and Enrique Blanco Viñuela.
Formal Verification of Safety PLC Based Control Software

Rahul Kumar, Thomas Ball, Jakob Lichtenberg, Nate Deisinger, Apoorv Upreti and Chetan Bansal.
Enabling Static Driver Verifier using Microsoft Azure

17:00-17:15 Closing

Room M101, Marjan Sirjani

Saturday June 4

UTP 2016

Room V102. Program .

Invited talk

9:00-10:00 Unifying Models and Laws for Concurrency and Distribution in Object-Oriented Programs. Tony Hoare (Microsoft Research, Cambridge, UK)

iFM Cloud

Room M104. Program .

Invited talk

10:30-11:30 Actors and Meta-Actors: Two-Level for Reasoning about Cloud Infrastructure. Gul Agha (University of Illinois at Urbana-Champaign)

PrePost

Room M105, Program .

Invited talks

10:30-11:30 From Pre-Verification and -Analysis to Post-Synthesis and -Optimization for Timed and Hybrid Systems. Kim G. Larsen (Aalborg University)

13:30-14:30 Reasoning with Big Code. Dino Distefano (Facebook and Queen Mary, University of London, UK)

V2CPS

Room V108, Program .

Keynote

9:00-10:00 Analysis-based approaches to achieving timing predictability. Sanjoy Baruah (University of North Carolina at Chapel Hill, USA)

Sunday, June 5

UTP 2016

Room V102, Program .

Invited talk

09:00-10:00 A New Roadmap on Linking Theories of Programming. He Jifeng (East China Normal University, China)

PhD Symposium at iFM

Room M104, Program .

Invited talks

08:30-09:30 How to Write and Present a Computer Science Paper. Mohammad Reza Mousavi (Halmstad University, Sweden)

13:30-14:30 Formal models and verification to support software evolution. Carlo Ghezzi (Politecnico di Milano, Italy)

COST Action Meeting ARVI

Room M105, Program .