Program2018-10-16T17:46:07+00:00

Program Overview

Oct. 10 
Wednesday
Oct. 11
Thursday
Oct. 12
Friday
 Oct. 12
Saturday
09:00 Registration Presentation 1: Shin Hong
Protecting Static Analysis False Positives by Learning from Alarm Review Data
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:00 Presentation 2 : Eun-Kyung Ji
Modeling and Verification of a Blockchain Consensus Protocol
10:30 Coffee Break
11:00 Session 1
Model Checking and Verification
Session 4
Components and Petri Nets
Session 5
Formalization of Networks; Semantics
Presentation 2 : Jun-Yeol Choi
자동차 시스템 검증의 현재와 미래
12:30 Lunch Lunch Closing  
 
 
 
Lunch
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