Monday September 9

  • 09:00 – 10:20 FM plenary keynote, invited by FACS (Room O. De Donato)
    • Ana Cavalcanti. Comparing Reactive Models and Cyclic Components of Robotic Systems: The RoboStar approach to model-based testing

  • 10:20 – 10:55 Coffee Break

  • 10:55 - 11:00 TAP Opening (Room 3.0.3)
    • Marieke Huisman, Falk Howar

  • 11:00 - 12:30 Session 1: Quality of Tests and Proofs (Room 3.0.3, Chair: Falk Howar)

    • Li Huang, Bertrand Meyer and Manuel Oriol. Is MCDC really better? Lessons from combining tests and proofs
    • Max Barth and Marie-Christine Jakobs. Refining CEGAR-based Test-Case Generation with Feasibility Annotations
    • Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov. No Smoke without Fire: Detecting Specification Inconsistencies with Frama-C/WP

  • 12:30 – 14:00 Lunch

  • 14:00 - 15:20 FM plenary keynote, invited by TAP (Room O. De Donato, Chair: Marieke Huisman)
    • Rosemary Monahan. Formalising Requirements for Systems Verification

  • 15:20 – 16:00 Coffee Break

  • 16:00 – 17:00 Session 2: Testing and Proving Advanced Properties (Room 3.0.3, Chair: Rüdiger Ehlers)

    • Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue and Daniel Gracia Pérez. Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack
    • Hao Wu, Thomas Flinkow and Dominique Mery. Cyclone: A New Tool for Verifying / Testing Graph-based Structures

Tuesday September 10

  • 9:00 – 10:20 FM plenary keynote, invited by LOPSTR/PPDP
    • Ningning Xie. Safe and Easy Compile-Time Generative Programming (Room O. De Donato)

  • 10:20 – 11:00 Coffee Break

  • 11:00 – 12:00 TAP keynote (Room 3.0.3, Chair: Falk Howar)
    • Rüdiger Ehlers. Efficient Temporal Logic Runtime Monitoring for Tiny Systems

  • 12:30 – 14:00 Lunch

  • 14:00 – 15:20 FM plenary keynote, invited by FMICS
    • Thierry Lecomte. B+ or how to model system properties in a formal software model (Room O. De Donato)

  • 15:20 – 16:00 Coffee Break

  • 16:00 – 17:30 Session 3: Applications of Tests and Proofs (Room 3.0.3, Chair: Rosemary Monahan)

    • Malte Lochau and Ina Schaefer. Model-based Testing of Quantum Computations
    • Maximilian Schlüter and Bernhard Steffen. Affinitree: A Compositional Framework for Formal Analysis and Explanation of Deep Neural Networks
    • Malte Mues, Julian Rüschoff and Ben Hermann. Exploring Loose Coupling of Static Slicing with Dynamic Symbolic Execution on the JVM


  • 19:00 - 22:00 FM Reception Buffet

Venue

All rooms are in the building ‘Edificio 3 - Gino Cassinis’ located at ‘Milano Città Studi - Piazza Leonardo da Vinci 32’

The main entrance and vehicle entrance to the Campus is in Piazza Leonardo, 32. There are other pedestrian entrances from Piazza Leonardo, Via Bonardi and Via Ponzio. There are car parks reserved for pass holders in the Leonardo Campus. Horizontal circulation within the Campus is fairly trouble-free. There are dropped kerbs between the pavement and the roadway. There are no routes with tactile signage for people with sight disabilities. There is no equipment for visually disabled persons.

The main entrance to the building is next to the main entrance to the Campus and has three steps up to it. Next to the steps are a ramp and a connecting drop-down with acceptable gradients. Access to the upper floors is by lift or the stairs. Horizontal circulation is trouble-free. Accessible toilet facilities are provided.