PhD Symposium at iFM'17 on
Formal Methods: Algorithms, Tools and Applications

Date: Tuesday, September 19, 2017
"Sala Biblioteca Arturo Graf" (first floor), via Verdi 8


8:15 - 9:00 Registration

09:00 - 10:00 Invited Speaker: Automatic Reasoning for Novel Engineering Designs. Mike Nicolai (Siemens, Belgium).

10:00 - 10:30 Coffee break

10:30 - 12:10
    • remove 10:30 - 10:50 Formal Verification of CNL Health Recommendations. Fahrurrozi Rahman and Juliana Küster Filipe Bowles.
    • remove 10:50 - 11:10 Modular Heap Shape Analysis for Java Programs. Florian Frohn and Jürgen Giesl.
    • remove 11:10 - 11:30 Abstraction-Based Model Checking of POMDPs in Motion Planning. Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Jost-Pieter Katoen and Bernd Becker.
    • remove 11:30 - 11:50 Using Coloured Petri Nets for Resource-Aware Program Analysis. Anastasia Gkolfi, Einar Broch Johnsen and Ingrid Chieh Yu.
    • remove 11:50 - 12:10 Co-Simulation and Formal Verification of Logic-Based Specifications of Components in CPSs. Maurizio Palmieri, Cinzia Bernardeschi and Andrea Domenici.
12:10 - 13:40 Lunch

13:40 - 15:20
    • remove 13:40 - 14:00 Security Functionality of IoT Devices. Elahe Fazeldehkordi, Olaf Owe and Toktam Ramezanifarkhani.
    • remove 14:00 - 14:20 Assessing the Coverage of Formal Specifications. Dominic Steinhöfel.
    • remove 14:20 - 14:40 Versioned Simulation Testing for Concurrent and Distributed Models. Lars Tveito, Einar Broch Johnsen and Rudolf Schlatte.
    • remove 14:40 - 15:00 An Abstraction Technique for Describing Concurrent Program Behaviour. Wytse Oortwijn.
    • remove 15:00 - 15:20 An Operational Semantics for a Weak Memory Model with Buffered Writes, Message Passing, and Goroutines. Daniel Fava, Martin Steffen, Volker Stolz and Stian Valle.
15:20 - 15:50 Coffee break

15:50 - 17:30
    • remove 15:50 - 16:10 On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theory. Francesco Leofante.
    • remove 16:10 - 16:30 On the Community Structure of SAT-BMC Problems. Xavier Gillard and Charles Pecheur.
    • remove 16:30 - 16:50 Virtually Timed Ambients: Formalisation and Analysis. Johanna Beate Stumpf, Einar Broch Johnsen and Martin Steffen.
    • remove 16:50 - 17:10 Towards a Contract-Based Unified Design Process. Cesar Santos, Mike Nicolai and Tom Schrijvers.
    • remove 17:10 - 17:30 Best Presentation award.


Important dates

  • Paper submission: June 2, 2017 Thursday, June 15, 2017 (expired)
  • Author notification: Friday, July 7, 2017
  • PhD Symposium: Tuesday, September 19, 2017
Deadlines expire at 23:59 anywhere on earth on the dates displayed above.


The theory, implementation, integration or application of formal methods in a broad sense.

Who can submit?

PhD students and young researchers at an early career stage (up to 2 years after PhD completion).

Why to submit?

Participants will have the possibility to give short presentations about their research projects.
    • remove The doctoral symposium offers an excellent opportunity to present your work in an international setting, and to get feedback from senior researchers in the field.
    • remove The doctoral symposium lets you exchange knowledge and experiences with fellow PhD-students in a related topic.
    • remove The best paper/presentation will be awarded.
    • remove The selected contributions will be published as a technical report of the University of Oslo, Norway.

What to submit?

You are welcome to submit an extended abstract of at most 3 pages, describing your research project which you would like to present. Co-authors are allowed, but you should be the first author. The results may have been accepted or even published elsewhere. Multiple submissions by one author are not permitted. Submissions should be written in English and follow the EasyChair formatting guidelines, available at

Please submit your abstract electronically in pdf via the EasyChair page

The submitted abstracts will undergo a lightweight reviewing process. A symposium proceedings containing the accepted abstracts will be available as a technical report of the University of Oslo.

Invited Speaker

remove Mike Nicolai (Siemens, Belgium) will talk about "Automatic Reasoning for Novel Engineering Designs".

Programme Committee