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|
|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.
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)
This event is kindly sponsored by the IMDEA Software Institute.