Program and Schedule of Student Sessions

There will be four student sessions, with two parallel tracks A and B that will take place in building A29 auditoriums E and D respectively. See the venue page for more information on the school location.

Session 1 (Monday 19th, 17:30 - 18:40)

Session 1 ASession 1 B

Model Checking AllTL Properties Over Set Automata

Hayssam Soueidan

Temporal Modeling and Verification of Biological Regulatory Networks (BRN)

Jamil Ahmad


Temporal Logic for Timed Control

Ghassan Oreiby

Robust Zone-Based Forward Reachability Analysis of Timed Automata

Mani Swaminathan


Temporal Logic with Constraints over Integers

Régis Gascon

Why discrete-time Petri nets with stopwatches?

Morgan Magnin

Session 2 (Tuesday 20th, 18:00 - 19:10)

Session 2 ASession 2 B

Model-checking Techniques for the Verification and Generation of Control Systems

Daniele Magazzeni

Tool Supported Real-Time System Verification Techniques Based on Abstraction/Deduction and Model-checking

Eun-Young Kang


Synthesis of Component Adaptor via Quotient of Specifications

Jean-Baptiste Raclet

Model Checking Timed Automata using Abstractions

Jasper Berendsen


Distributed Synthesis for Well-Connected Architectures

Nathalie Sznajder

Practical Program Analysis for Liveness and Fairness

Alexey Gotsman

Session 3 (Wednesday 21st, 14:00 - 15:35)

Session 3 ASession 3 B

Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion

Tomáš Brázdil

Complexity of some Bisimilarity Problems between BPP and BPA or Finite-State System

Martin Kot


Automata for Querying Compressed Documents

Barbara Fila

Weakly Extended Process Rewrite Systems

Vojtěch Řehák


Expand, Enlarge and Check

Gilles Geeraerts

Security of Cryptographic Protocols: New Properties

Eugen Zălinescu


From Pointer Systems to Counter Systems

Arnaud Sangnier

Timed Distributed π-calculus

Cristian Prisacariu

Session 4 (Thursday 22nd, 17:15 - 18:25)

Session 4 ASession 4 B

Compositional model checking of monadic least fixed point logic

Matko Botinčan

On Applying Formal Verification to Secured Group Communications

Benjamin Fontan


LfV, Language for Verification

Duy-Tung Nguyen

Typed Temporal Logic: A General Framework for Verification of Nonfunctional and Security Requirements of Component Based Systems

Mohammad Izadi


Model-checking Coupled and Coherent Systems

Frabrice Gadaud

Modelling Logical and Geometrical Spacial Allocation with AltaRica

Laurent Sagaspe

Call for Student Papers [Deadline passed]

One of the aims of MOVEP is to be a meeting place where Ph.D. students can discuss together and with senior researchers. As in the previous occurrences of MOVEP, special sessions will be devoted to Ph.D. student talks. The presentation should introduce:

  1. the research area and main theme,
  2. the directions of the work,
  3. some results (obtained or expected).

Moreover, extended abstracts of these presentations will be published with the proceedings of the school. These abstracts should not exceed 6 pages and should be written in English using LaTeX2e. Please use the provided template and style file for your abstract. Submissions have to be sent electronically before April 22nd to

There are scholarships available to support Ph.D. students participating in the Ph.D. student session.

Printer-friendly version Printer-friendly version