13th International Conference on integrated Formal Methods (iFM 2017)
PROCEEDINGS
The iFM 2017 proceedings are available (on-line edition --- free access for conference participants granted for 4 weeks).PROGRAM OVERVIEW
Monday, September 18 |
Tuesday, September 19 |
Wednesday, September 20 |
Thursday, September 21 |
Friday, September 22 |
||
---|---|---|---|---|---|---|
08:15 - 09:00 | Registration (8:15-8:45, via Verdi 9) Opening Plenary with Paola Pisano, Deputy Mayor for Innovation and Smart City at the City of Torino (8:45-9:00, room "Sala Multifunzione 1", via Verdi 9) |
Registration (via Verdi 9) | Registration (8:15-8:45, via Verdi 9) iFM Opening (8:45-9:00, room "Aula Magna della Cavallerizza", via Verdi 9) |
Registration (via Verdi 9) | Registration (via Verdi 9) | |
09:00 - 10:00 | SATELLITE EVENT SESSIONS | SATELLITE EVENT SESSIONS | iFM Keynote I: André Platzer |
iFM Keynote II: Jane Hillston |
iFM Keynote III: Martin Vechev |
|
10:00 - 10:30 | Coffee break | Coffee break | Coffee break | Coffee break | Coffee break | |
10:30 - 12:10 | SATELLITE EVENT SESSIONS | SATELLITE EVENT SESSIONS | iFM Session I: Cyber-physical systems |
iFM Session IV: Concurrency and distributed systems |
iFM Session VII: Verified Software |
|
12:10 - 13:40 | Lunch | Lunch | Lunch
FME Busines Meeting, room "Aula Magna del Rettorato" (first floor), via Verdi 8 |
Lunch | iFM Closing (12:10-12:20)
Lunch |
|
13:40 - 15:20 | SATELLITE EVENT SESSIONS | SATELLITE EVENT SESSIONS | iFM Session II: Software Verification Tools |
iFM Session V: Program Verification Techniques |
||
15:20 - 15:50 | Coffee break | Coffee break | Coffee break | Coffee break | ||
15:50 - 17:30 | SATELLITE EVENT SESSIONS | SATELLITE EVENT SESSIONS | iFM Session III: Safety-critical systems |
iFM Session VI: Formal Modeling |
||
FMICS-AVoCS Reception (Hotel NH Torino Santo Stefano, 19:00-22:00) |
Wine tasting event (18:30-20:30), see the letter from the Wine Chair |
iFM Reception (Baratti & Milano, 18:30) |
||||
ARVI, ALP4IoT and WAO Social dinner (Le Rondini, 19:30, not included in the registration) |
FMICS-AVoCS Social dinner, award of best paper (Porto di Savona, 20:00) |
iFM Social dinner, award of best paper and best tool paper (Al Gufo Bianco, 19:30) |
iFM Keynotes (room "Aula Magna della Cavallerizza", via Verdi 9)
- remove
André Platzer
Logic & Proofs for Cyber-Physical Systems with KeYmaera X
(session chair: Ana Cavalcanti) - remove
Jane Hillston
Integrating Inference with Stochastic Process Algebra Models
(session chair: Steve Schneider) - remove
Martin Vechev
Machine Learning for Programming
(session chair: Reiner Hahnle)
iFM Sessions (room "Aula Magna della Cavallerizzza", via Verdi 9)
iFM Session I: Cyber-Physical Systems (session chair: Einar Broch Johnsen)
- remove
Simone Silvetti, Alberto Policriti and Luca Bortolussi
An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems - remove
Pedro Ribeiro, Alvaro Miyazawa, Wei Li, Ana Cavalcanti and Jon Timmis
Modelling and Verification of Timed Robotic Controllers - remove
Sven Linker
Spatial Reasoning about Motorway Traffic Safety with Isabelle/HOL - remove
Albert Rizaldi, Jonas Keinholz, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf and Tobias Nipkow
Formalising Traffic Rules for Autonomous Vehicles Involving Multiple Lanes in Isabelle/HOL
iFM Session II: Software Verification Tools (session chair: Carlo Furia)
- remove
Mark Utting, David Pearce and Lindsay Groves
Making Whiley Boogie! - remove
Florian Frohn and Jürgen Giesl
Complexity Analysis for Java with AProVE - remove
Stefan Blom, Saeed Darabi, Marieke Huisman and Wytse Oortwijn
The VerCors Tool Set: Verification of Parallel and Concurrent Software - remove
Ferruccio Damiani, Michael Lienhardt, Radu Muschevici and Ina Schaefer
An Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs
iFM Session III: Safety-Critical Systems (session chair: Olaf Owe)
- remove
Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser and Alexander Weigl
Generalised Test Tables - a Practical Specification Language for Reactive Systems - remove
Fahrurrozi Rahman and Juliana Küster Filipe Bowles
Formal Verification of CNL Health Recommendations - remove
James Baxter and Ana Cavalcanti
Algebraic Compilation of Safety-Critical Java Bytecode - remove
Andrii Kovalov, Elisabeth Lobe, Andreas Gerndt and Daniel Lüdtke
Task-Node Mapping in an Arbitrary Computer Network using SMT Solver
iFM Session IV: Concurrency and distributed systems (session chair: Marieke Huisman)
- remove
Dalay Israel de Almeida Pereira, Marcel Vinicius Medeiros Oliveira, Madiel Conserva Filho and Sarah Raquel Da Rocha Silva
BTS: A Tool for Formal Component-based Development - remove
Stavros Aronis, Scott Fritchie and Kostis Sagonas
Testing and Verifying Chain Repair Methods for CORFU Using Stateless Model Checking - remove
Wei Ji, Farn Wang and Peng Wu
Synthesizing Coalitions for Multi-Agent Games - remove
Ludovic Henrio, Cosimo Laneve and Vincenzo Mastandrea
Analysis of synchronisation patterns in stateful active objects
iFM Session V: Program Verification Techniques (session chair: Heike Wehrheim)
- remove
Olaf Owe, Toktam Ramezanifarkhani and Elahe Fazeldehkordi
Hoare-style Reasoning from Multiple Contracts - remove
Dominic Steinhöfel and Nathan Wasser
A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows - remove
Yuting Chen and Carlo A. Furia
Triggerless Happy: Intermediate Verification with a First-Order Prover - remove
Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch and Mattias Ulbrich
SemSlice: Exploiting Relational Verification for Automatic Program Slicing
iFM Session VI: Formal Modeling (session chair: Juliana Bowles)
- remove
Ajay Krishna, Pascal Poizat and Gwen Salaün
VBPMN: Automated Verification of BPMN Processes - remove
Barbara Kordy and Wojciech Widel
How well can I secure my system? - remove
Hao Wu
MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams - remove
Stephen Gilmore, Daniel Reijsbergen and Andrea Vandin
Transient and Steady-State Statistical Analysis for Discrete Event Simulators
iFM Session VII: Verified Software (session chair: Mark Utting)
- remove
Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn and Wolfgang Reif
Modular Verification of Order-Preserving Write-Back Caches - remove
Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi and Elena Pagani
Formal verification of ARP (Address Resolution Protocol) through SMT-based model checking - A case study - remove
Joao F. Ferreira, Saul A. Johnson, Alexandra Mendes and Phillip J. Brooke
Certified Password Quality - A Case Study Using Coq and Linux Pluggable Authentication Modules - remove
Murat Moran and Dan Wallach
Verification of STAR-Vote and Evaluation of FDR and ProVerif
Monday, September 18, SATELLITE EVENT SESSIONS
- remove FMICS-AVoCS, room "Sala Multifunzione 1", via Verdi 9
- remove ARVI [participation is by invitation only], room "Aula Magna del Rettorato" (first floor), via Verdi 8
- remove ALP4IoT and WAO, 9:00-10:00 room "Aula Magna del Rettorato" (first floor), 10:30-... room "Sala Principe d'Acaja" (ground floor), via Verdi 8
Tuesday, September 19, SATELLITE EVENT SESSIONS
- remove FMICS-AVoCS, room "Sala Multifunzione 1", via Verdi 9
- remove FVAV, room "Aula Magna del Rettorato" (first floor), via Verdi 8
- remove PrePost, room "Sala Principe d'Acaja" (ground floor), via Verdi 8
- remove PhD-iFM, room "Sala Biblioteca Arturo Graf" (first floor), via Verdi 8
Wednesday, September 20, SATELLITE EVENT SESSIONS
- remove FMICS-AVoCS, room "Sala Multifunzione 1", via Verdi 9