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.
Symposium: | December 3, 2019 |
Main Conference: | December 4-6, 2019 |
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 |
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.
Jacopo Mauro (University of Southern Denmark, Odense, Denmark)
César Sánchez (IMDEA Software Institute, Madrid, Spain)
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)
Christian Johansen (University of Oslo, Norway)
Sandro Stucki (Chalmers, Sweden)
This event is kindly sponsored by the IMDEA Software Institute.