Program Overview

 Main Conference  Workshop 
Oct. 10 
Oct. 11
Oct. 12
 Oct. 12
09:00 Registration Workshop Program
09:25 Opening
09:30 Invited talk : Edward Lee

What Good Are Formal Models?

Invited talk : Grigore Rosu

Formal Design, Implementation and Verification of Blockchain Languages

Invited talk : Moonzoo Kim

Lessons Learned from Automated Analysis of Industrial SW for 15 Years

10:30 Coffee Break
11:00 Session 1
Model Checking and Verification
Session 4
Components and Petri Nets
Session 5
Formalization of Networks; Semantics
12:30 Lunch Lunch Closing  
14:00 Session 2
Security and Languages
Guided tour in Gyeongju

15:30 Coffee break
16:00 Section 3
Tool Papers
17:00 SC meeting
18:00 Dinner in Pohang (Optional)

18:30 Reception (at the venue) Banquet in Gyeongju

Session 1: Model Checking and Verification (chair: Grigore Rosu)

– Thomas Neele, Tim Willemse and Jan Friso Groote: Solving Parameterised Boolean Equation Systems with Infinite Data Through Quotienting
– Antti Siirtola and Keijo Heljanko: Dynamic Cut-Off Algorithm for Parameterised Refinement Checking
– Simon Foster, James Baxter, Ana Cavalcanti, Alvaro Miyazawa and Jim Woodcock: Automating Verification of State Machines with Reactive Designs and Isabelle/UTP

Session 2: Security and Languages (chair: Edward Lee)

 – Valentina Castiglioni, Konstantinos Chatzikokolakis and Catuscia Palamidessi: A Logical Characterization of Differential Privacy via Behavioral Metrics
 – Rim El Ballouli, Saddek Bensalem, Marius Bozga and Joseph Sifakis: Programming Dynamic Reconfigurable Systems
 – Vlad Nicolae Serbanescu, Frank De Boer and Mohammad Mahdi Jaghoori: Actors with Coroutine Support in Java

Section 3: Tool Papers (chair: Eric Madelaine)

 – Diego Marmsoler and Habtom Kahsay Gidey: FACTum Studio: A Tool for the Axiomatic Specification and Verification of Architectural Design Patterns
 – Sander de Putter, Anton Wijs and Dan Zhang: The SLCO Framework for Verified, Model-driven Construction of Component Software

Session 4: Components and Petri Nets (chair: Catuscia Palamidessi)

 – Jean-Paul Bodeveix, Arnaud Dieumegard and Mamoun Filali-Amine: Event-B Formalization of a Variability-Aware Component Model Patterns Framework
– Anastasia Gkolfi, Einar Broch Johnsen, Lars Michael Kristensen and Ingrid Chieh Yu: Using Coloured Petri Nets for Resource Analysis of Active Objects

 – Prabhakar Dixit, Eric Verbeek and Wil van der Aalst: Incremental Computation of Synthesis Rules for Free-Choice Petri nets

Session 5: Formalization of Networks; Semantics (chair: Marius Bozga)

 – Liyi Li and Elsa Gunter: IsaK-Static: A Complete Static Semantics of K
 – Mojgan Kamali and Ansgar Fehnker: Adaptive Formal Framework for WMN Routing Protocols
 – Christian Attiogbe: Building Correct SDN Components from a Global Event-B Formal Model