PhD-iFM’19
Welcome to the homepage of PhD-iFM’19, a PhD Symposium at iFM 2019 on Formal Methods: Algorithms, Tools and Applications, held in Bergen, Norway on December 3, 2019.
Participants will have the possibility to give short presentations about their research projects.
- 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.
- The doctoral symposium lets you exchange knowledge and experiences with fellow PhD-students in a related topic.
- The selected contributions will be published as a technical report of the Western Norway University of Applied Sciences, Norway.
Important Dates
| Symposium: | December 3, 2019 |
| Main Conference: | December 4-6, 2019 |
Provisional Program (December 3rd)
| Time | Activity |
|---|---|
| 08:00 - 09:00 | Registration |
| 09:00 - 10:00 | Invited Talk. Andreas Griesmayer, ARM, UK Formal Modelling for Modern CPU Designs |
| 10:00 - 10:30 | Coffee break |
| 10:30 - 10:35 | Opening |
| 10:35 - 11:00 | Talk 1. Probabilistic Compositional Feature-Oriented Systems Student: Clemens Dubslaff - Mentor: Martin Steffen |
| 11:00 - 11:25 | Talk 2. Automatic Loop Invariant Generation Using Predicate Abstraction For Dependence Analysis Student: Asmae Heydari Tabar - Mentor: Carlo Furia |
| 11:25 - 11:50 | Talk 3. Graph Operations and Diagrammatic Modelling Student: Tam Thanh Truong - Mentor: Christian Johansen |
| 11:50 - 12:15 | Talk 4. Coverage Analysis of SML Expressions in CPN Models Student: Faustin Ahishakiye - Mentor: Sandro Stucki |
| 12:30 - 14:00 | Lunch |
| 14:00 - 14:25 | Talk 5. Static Detection of Distributed Denial of Service Attacks in Active Object Systems Student: Elahe Fazeldehkordi - Mentor: Ferrucio Damiani |
| 14:25 - 14:50 | Talk 6. Learning From Families: Inferring Behavioral Variability From Software Product Lines Student: Carlos Diego Damasceno - Mentor: Gordon Pace |
| 14:50 - 15:15 | Talk 7. Towards Better Data Structures for Numerics such as Optimal Transport Student: Justus Sagemüller - Mentor: Gerardo Schneider |
| 15:15 - 15:45 | FACE-TO-FACE meetings |
| 15:45 - 16:00 | Coffee |
| 16:00 - 16:25 | Talk 9 . Sound Probabilistic Numerical Error Analysis Student: Debasmita Lohar - Mentor: Cesar Sanchez |
| 16:25 - 16:50 | Talk 10. Resource Sharing via Capability-Based Multiparty Session Types Student: A. Laura Voinea - Mentor: Olaf Owe |
| 16:50 - 17:15 | Talk 11. SIGmA: GPU Accelerated Simplification of SAT Formulas Student: Muhammad Osama - Mentor: Jacopo Mauro |
| 17:15 - 17:30 | Best Presentation Award |
Invited Speaker
Andreas Griesmayer, Senior Research Engineer (Arm, Cambridge, UK)
Title: Formal Modelling for Modern CPU Designs
Abstract: The Arm architecture describes operation and programming interface of
billions of CPUs produced every year. In addition to smartphones,
chips implementing the Arm architecture power everything from tiny IoT
devices to super computers, with an emphasis on power efficiency.
Arm maintains and develops the Arm architecture, provides
corresponding compilers, and contributes to operating systems.
Multiple design teams around the globe design compatible CPUs, GPUs
and other essential semiconductor IP. Instead of building physical
hardware, Arm works with a network of partners that build hardware
based on Arm designs and architectures. Being at the centre of this
eco systems, it is essential to ensure the integrity of the
architectures and compliance of the designs. Formal models play an
important role in this process.
The talk will outline the challenges of formal verification in modern
CPU designs and how formal models capture the expected behaviour of a
processor from the perspective of the architecture, the hardware
implementation, as well as the programmer’s view on the memory model.
It won’t cover details of CPU design, but will highlight challenges,
solutions, and possibly surprising characteristics of modern hardware.
Accepted papers
- Elahe Fazeldehkordi, Olaf Owe and Toktam Ramezanifarkhani: “Static Detection of Distributed Denial of Service Attacks in Active Object Systems”
- Tam Thanh Truong: “Graph Operations and Diagrammatic Modelling”
- Debasmita Lohar, Milos Prokop and Eva Darulova: “Sound Probabilistic Numerical Error Analysis”
- Carlos Diego Damasceno: “Learning From Families: Inferring Behavioral Variability From Software Product Lines”
- Faustin Ahishakiye, Volker Stolz and Lars Michael Kristensen: “Coverage Analysis of SML Expressions in CPN Models”
- A. Laura Voinea, Ornela Dardha and Simon Gay: “Resource Sharing via Capability-Based Multiparty Session Types”
- Muhammad Osama and Anton Wijs: “SIGmA: GPU Accelerated Simplification of SAT Formulas”
- Clemens Dubslaff: “Probabilistic Compositional Feature-Oriented Systems”
- Asmae Heydari Tabar, Richard Bubel and Reiner Hähnle: “Automatic Loop Invariant Generation Using Predicate Abstraction For Dependence Analysis”
- Justus Sagemüller, Olivier Verdier and Volker Stolz: “Towards Better Data Structures for Numerics such as Optimal Transport”
Organization
Symposium Co-Chairs
Jacopo Mauro (University of Southern Denmark, Odense, Denmark)
César Sánchez (IMDEA Software Institute, Madrid, Spain)
Program Committee
Erika Ábrahám (RWTH Aachen University, Germany)
Carlo Furia (USI, Switzerland)
Ferruccio Damiani (University of Turin, Italy)
Gordon Pace (University of Malta, Malta)
Gerardo Schneider (University of Gothenburg, Sweden)
Martin Steffen (University of Oslo, Norway)
Olaf Owe (University of Oslo, Norway)
Additional Mentors
Christian Johansen (University of Oslo, Norway)
Sandro Stucki (Chalmers, Sweden)
Sponsor
This event is kindly sponsored by the IMDEA Software Institute.
