Program

October 31, 2019

8:00 Registration
08:30 Opening
09:00 Tutorial-1
Patrick Cousot
Abstract interpretation
10:30 Break
11:00 Tutorial-1
Patrick Cousont
Abstract interpretation
12:00 Tutorial-2
Kamel Barkaoui
Techniques for Reduced Petri Nets State Spaces Generation
13:00 Lunch
14:00 Tutorial-2
Kamel Barkaoui
Techniques for Reduced Petri Nets State Spaces Generation

November 1, 2019

8:00 Registration
08:30 Opening
09:00 Tutorial-3
Dominique Méry
Verification by Construction of Distributed Algorithms
10:30 Break
11:00 Tutorial-3
Dominique Méry
Verification by Construction of Distributed Algorithms
12:00 Tutorial-4
Akka Zemmari
Concentration Inequalities in the Analysis of Randomized Distributed Algorithms
13:00 Lunch
14:00 Tutorial-4
Akka Zemmari
Concentration Inequalities in the Analysis of Randomized Distributed Algorithms

November 2, 2019

8:00 Registration
08:30 Opening
09:00 Invited Speaker
Patrick Cousot
Calculational design of a regular model checker by abstract interpretation
10:30 Break
11:00 Session1: Models and Transition system
Arpit Sharma.
The Linear Time-Branching Time Spectrum of Equivalences for Stochastic Systems with Non-determinism
Uli Fahrenberg, Axel Legay and Karin Quaas.
Computing Branching Distances Using Quantitative Games
Fateh Latreche, Abdelkader Moudjari and HichemTalbi.
Clinical Pathways Formal Modelling using Bigraphical Reactive Systems
Hiroyuki Seki, Reo Yoshimura and Yoshiaki Takata.
Optimal Run Problem for Weighted Register Automata
13:00 Lunch
14:00 Session 2: Real-time and temporal logics
Jawher Jerray, Etienne André and Sahar Mhiri.
Time4sys2imi: A tool to formalize real-time system models under uncertainty
Bogdan Aman and Gabriel Ciobanu.
Verification of Multi-Agent Systems With Timeouts for Migration and Communication
František Blahoudek, Juraj Major and Jan Strejček.
LTL to Smaller Self-Loop Alternating Automata
Samir Ouchani.
Towards a Call Behavior-Based Compositional Verification Framework for SysML Activity Diagrams
Huu Vu Nguyen and Tayssir Touili.
BCARET Model Checking for Malware Detection

November 3, 2019

09:00 Invited Speaker
Thomas A. Henzinger
Temporal Logics for Multi-Agent Systems
10:30 Break
11:00 Session 3: Verification and Concurrency
Jafar Hamin.
Starvation-Free Monitors
Kirstin Peters, Christoph Wagner and Uwe Nestmann.
Taming Concurrency for Verification Using Multiparty Session Types
XiaoyingMou and Haiming Chen
Context-free grammars for deterministic regular expressions with interleaving
Moez Krichen.
Testing Real-Time Systems using Determinization Techniques for Automata over Timed Domains
13:00 Lunch
14:00 Session 4: Privacy and Security
Vincenzo Arceri, Martina Olliaro, Agostino Cortesi and Isabella Mastroeni.
Completeness of Abstract Domains for String Analysis of JavaScript Programs
Marwa Chaieb, Mirko Koscina, SouheibYousfi, Pascal Lafourcade and Riadh Robbana.
DABSTERS: a Privacy Preserving e-Voting Protocol for Permissioned Blockchain
Daniele Gorla, Federica Granese and CatusciaPalamidessi.
Enhanced models for privacy and utility in continuous-time diffusion networks
16:00 Social event and gala dinner

November 4, 2019

09:00 Invited Speaker
Dominique Méry
Verification by Construction of Distributed Algorithms
10:30 Break
11:00 Session 5: Equations, types, and programming languages
Alexis Maffart and Xavier Thirioux.
Taylor series expansions
Seyed Hossein Haeri and Paul Keir.
Solving the Expression Problem in C++, à la LMS
Härmel Nestra.
Laws of Monadic Error Handling
Martin Sulzmann and Kenny Zhuo
Ming Lu. Solving of Regular Equations Revisited
13:00 Lunch
14:00 Closing