| Time | Speaker | Location and session chair |
|---|---|---|
| 08:15-08:55 | Registration (Location: outside room M208) | |
| 09:00-10:00 | Rocco De Nicola (IMT Lucca, IT) Invited talk: Languages and Models for Collective Adaptive Systems (Slides) |
Room M208 (Luca Aceto) |
| 10:00-10:25 | Flemming Nielson, Hanne Riis Nielson and Ximeng Li Limitations of Non-Interference |
Room M208 (Luca Aceto) |
| 10:25-10:55 | Coffee Break | |
| 10:55-11:20 | Hans Hüttel Binary session types for psi-calculi |
Room M208 (Rocco De Nicola) |
| 11:20-11:45 | Casper Bach Poulsen, Peter Mosses and Neil Sculthorpe Using Typings as Types (Slides) |
Room M208 (Rocco De Nicola) |
| 11:45-12:10 | Hans Hüttel and Sam Sepstrup Olesen Compiling Protocol Narrations into Applied Pi Processes |
Room M208 (Rocco De Nicola) |
| 12:10-12:35 | Luciano García-Bańuelos, Nick R.T.P. van Beest, Marlon Dumas
and Marcello La Rosa Business Process Conformance Checking Based on Event Structures |
Room M208 (Rocco De Nicola) |
| 12:35-14:00 | Lunch Break (Location: Reykjavik University, Mars 2) | |
| 14:00-14:25 | Wojciech Mostowski From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java (Slides) |
Room M208 (Hanne Riis Nielson) |
| 14:25-14:50 | Olaf Owe, Jia-Chun Lin and Ingrid Yu A Formal Framework Supporting Unrestricted Software Changes in Object-Oriented Concurrent Systems (Slides) |
Room M208 (Hanne Riis Nielson) |
| 14:50-15:15 | Jesus Mauricio Chimento, Wolfgang Ahrendt, Gordon Pace and Gerardo Schneider StaRVOOrS: Unifying Static and Runtime Verification of Java |
Room M208 (Hanne Riis Nielson) |
| 14:15-15:40 | Charlie McDowell and Olaf Owe Flooding Detection in Concurrent Object Systems (Slides) |
Room M208 (Hanne Riis Nielson) |
| 15:40-16:10 | Coffee Break | |
| 16:10-16:35 | Eduard Kamburjan, Crystal Chang Din and Tzu-Chun Chen Session-Based Compositional Verification on Actor-based Concurrent Systems (Slides) |
Room M208 |
| 16:35-17:00 | Ferdinand Vesely Towards Small-step Compilation Schemas for SOS (Slides) |
Room M208 |
| 17:00-17:25 | Robin Kaarsgaard Join inverse categories and reversible recursion (Slides) |
Room M208 |
| 17:25-17:50 | Thomas van Binsbergen, Peter Mosses and Neil Sculthorpe Tool Support for Component-Based Semantics (Slides) |
Room M208 |
| 17:50-18:00 | Break | |
| 18:00-19:30 | Welcome Reception (Location: Olympus, Mars 3) | |
| Time | Speaker | Location and session chair |
|---|---|---|
| 09:00-10:00 | Jiri Srba (Aalborg University, DK) Invited talk: Techniques and Tools for the Analysis of Timed Workflows (Slides) |
Room V201 (Anna Ingolfsdottir) |
| 10:00-10:25 | Hernan Ponce-De-Leon, Keijo Heljanko and Cristian Rosa Improving Partial Order Reductions in Multithreaded Programs with Local First Search |
Room V201 (Anna Ingolfsdottir) |
| 10:25-10:55 | Coffee Break | |
| 10:55-11:20 | John J. Camilleri and Gerardo Schneider Modelling and analysis of normative contracts (Slides) |
Room V201 (Jiri Srba) |
| 11:20-11:45 | Raúl Pardo and Gerardo Schneider Privacy in Evolving Social Networks (Slides) |
Room V201 (Jiri Srba) |
| 11:45-12:10 | Steen Vester Winning Cores in Parity Games (Slides) |
Room V201 (Jiri Srba) |
| 12:10-12:35 | Mathias N. Justesen Formal Verification using Parity Games (Slides) |
Room V201 (Jiri Srba) |
| 12:35-14:00 | Lunch Break (Location: Reykjavik University, Canteen, first floor) | |
| 14:00-14:25 | Heinrich Ody, Michael R. Hansen and Martin Fränzle Discounted Duration Calculus (Slides) |
Room V201 (Olaf Owe) |
| 14:25-14:50 | Marco Paviotti and Jesper Bengtson Formally Verifying Exceptions for Low-level code with Separation Logic |
Room V201 (Olaf Owe) |
| 14:50-15:15 | Fernando Macias, Adrian Rutle and Volker Stolz A Property Specification Language for Runtime Verification of Executable Models (Slides) |
Room V201 (Olaf Owe) |
| 14:15-15:40 | Xiaoliang Wang, Adrian Rutle and Yngve Lamo Towards user-friendly and efficient analysis with Alloy |
Room V201 (Olaf Owe) |
| 15:40-16:10 | Coffee Break | |
| 16:10-16:35 | Eva Burrows Algebraic Combinators for Data Dependencies and Their Applications (Slides) |
Room V201 (Peter Mosses) |
| 16:35-17:00 | Tero Hasu and Magne Haveraaen Errors as Data Values as the Language Default |
Room V201 (Peter Mosses) |
| 17:00-17:25 | Fazle Rabbi, Yngve Lamo, Lars Michael Kristensen and Ingrid Chieh Yu A generalization of termination conditions for partial model completion (Slides) |
Room V201 (Peter Mosses) |
| 17:25-17:50 | Philipp Haller and Heather Miller A formal model for direct-style asynchronous observables (Slides) |
Room V201 (Peter Mosses) |
| 17:50-19:30 | Break | |
| 19:30- | Workshop Dinner at Restaurant Kolabrautinn | |
| Time | Speaker | Location and session chair |
|---|---|---|
| 09:00-10:00 | Marta Kwiatkowska (University of Oxford, UK) Invited talk: Computing Reliably with Molecular Walkers (Slides) |
Room M104 (Marjan Sirjani) |
| 10:00-10:25 | Masoumeh Taromirad and Mohammadreza Mousavi Implementation-based Refinements for Equivalence Class Testing |
Room M104 (Marjan Sirjani) |
| 10:25-10:55 | Coffee Break | |
| 10:55-11:20 | Andrew Edmunds, Colin Snook and Marina Walden Towards Component-based Reuse for Event-B (Slides) |
Room M104 (Marta Kwiatkowska) |
| 11:20-11:45 | Niccolň Veltri and Silvio Capobianco An implementation in Agda of Sutner's decision algorithms for injectivity and surjectivity of one-dimensional cellular automata |
Room M104 (Marta Kwiatkowska) |
| 11:45-12:10 | Jonatan Wiik and Pontus Boström Contract-based specification and verification of dataflow programs (Slides) |
Room M104 (Marta Kwiatkowska) |
| 12:10-12:35 | Ali Jafari, Ehsan Khamespanah, Marjan Sirjani and Holger Hermanns Probabilistic Floating-Time Transition System: A New Approach For State Space Reduction of Probabilistic Actors |
Room M104 (Marta Kwiatkowska) |
| 12:35-14:00 | Lunch Break (Location: Nautholl) | |
| 14:00-14:25 | Marco Peressotti On endofunctors modelling higher-order behaviours |
Room M104 (Mohammad Reza Mousavi) |
| 14:25-14:50 | Marino Miculan, Marco Peressotti and Andrea Toneguzzo Open memory transaction in Haskell |
Room M104 (Mohammad Reza Mousavi) |
| 14:50-15:15 | Denis Firsov and Tarmo Uustalu Acyclic attribute evaluation in a dependently typed setting (Slides) |
Room M104 (Mohammad Reza Mousavi) |
| 14:15-15:40 | Tanya Braun, Arne Wichmann and Sibylle Schupp Specialized Strategies for Learning Integrated Circuits using Angluin L* and Rivest/Shapire Homing Inference (Slides) |
Room M104 (Mohammad Reza Mousavi) |
| 15:40-16:10 | Coffee Break | |
| 16:10-16:35 | Dario Della Monica and Adrian Francalanza Towards A Hybrid Approach to Software Verification(Extended Abstract) |
Room M104 (Gerardo Schneider) |
| 16:35-17:00 | Luca Aceto, Ignacio Fábregas, Carlos Gregorio-Rodríguez and Anna Ingolfsdottir A logical characterisation for input output conformance simulation iocos (Slides) |
Room M104 (Gerardo Schneider) |
| 17:00-17:25 | Álvaro García-Pérez Rule formats for bounded nondeterminism in nominal structural operational semantics |
Room M104 (Gerardo Schneider) |
| 17:25-17:30 | Closing | |
Last Modified: 20/10/2015 at 15:09 GMT