Formal Verification in Heterogeneous Systems
Event details
| Date | 29.08.2024 |
| Hour | 14:00 › 16:00 |
| Speaker | Alexandre Pinazza |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. Viktor Kuncak
Thesis advisor: Prof. Clément Pit-Claudel
Thesis coadvisor: Prof. Thomas Bourgeat
Co-examiner: Prof. George Candea
Abstract
Heterogeneous systems are everywhere: in our phones, laptops, cameras, and embedded devices. We rely on such heterogeneous systems mainly to obtain better scalability and power efficiency. However, as systems become more complicated, achieving the best result becomes increasingly difficult. Moreover, our lives increasingly depend on those systems working correctly. For example, pacemakers can now wirelessly connect to one's phone, this communication must be secure and not use too much energy. It is therefore essential to verify that these systems never exhibit any undesirable behaviors.
The overarching goal of this research proposal is to have easy-to-use, efficient, formally verified heterogeneous systems. This goal can be split into three sub-goals. 1) How can we create easy-to-use and efficient frameworks for heterogeneous systems? 2) How can we formally verify hardware components and provide a nice interface for them? 3) How can we verify the overall correctness of interacting components?
For the first sub-goal, we will take inspiration from Dandelion, a compiler and runtime engine for automatically scaling programs to various heterogeneous systems. For the second goal, we will investigate how information-preserving refinements help us verify that our hardware components are correct. For the last sub-goal, we will study how the DimSum framework helps us verify multi-language programs.
Background papers
- Dandelion: a compiler and runtime for heterogeneous systems by Rossbach et al.
https://dl.acm.org/doi/abs/10.1145/2517349.2522715
- Verifying Hardware Security Modules with Information-Preserving Refinement by Athalye et al.
https://www.usenix.org/conference/osdi22/presentation/athalye
- DimSum: A Decentralized Approach to Multi-language Semantics and Verification by Sammler et al.
https://dl.acm.org/doi/10.1145/3571220
Exam president: Prof. Viktor Kuncak
Thesis advisor: Prof. Clément Pit-Claudel
Thesis coadvisor: Prof. Thomas Bourgeat
Co-examiner: Prof. George Candea
Abstract
Heterogeneous systems are everywhere: in our phones, laptops, cameras, and embedded devices. We rely on such heterogeneous systems mainly to obtain better scalability and power efficiency. However, as systems become more complicated, achieving the best result becomes increasingly difficult. Moreover, our lives increasingly depend on those systems working correctly. For example, pacemakers can now wirelessly connect to one's phone, this communication must be secure and not use too much energy. It is therefore essential to verify that these systems never exhibit any undesirable behaviors.
The overarching goal of this research proposal is to have easy-to-use, efficient, formally verified heterogeneous systems. This goal can be split into three sub-goals. 1) How can we create easy-to-use and efficient frameworks for heterogeneous systems? 2) How can we formally verify hardware components and provide a nice interface for them? 3) How can we verify the overall correctness of interacting components?
For the first sub-goal, we will take inspiration from Dandelion, a compiler and runtime engine for automatically scaling programs to various heterogeneous systems. For the second goal, we will investigate how information-preserving refinements help us verify that our hardware components are correct. For the last sub-goal, we will study how the DimSum framework helps us verify multi-language programs.
Background papers
- Dandelion: a compiler and runtime for heterogeneous systems by Rossbach et al.
https://dl.acm.org/doi/abs/10.1145/2517349.2522715
- Verifying Hardware Security Modules with Information-Preserving Refinement by Athalye et al.
https://www.usenix.org/conference/osdi22/presentation/athalye
- DimSum: A Decentralized Approach to Multi-language Semantics and Verification by Sammler et al.
https://dl.acm.org/doi/10.1145/3571220
Practical information
- General public
- Free
Contact
- edic@epfl.ch