Formal methods for software-controlled cyber-physical systems
Event details
| Date | 06.07.2023 |
| Hour | 14:00 › 16:00 |
| Speaker | Samuel Chassot |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. George Candea
Thesis advisor: Prof. Viktor Kuncak
Co-examiner: Prof. Clément Pet-Claudel
Abstract
The software has extended its reach into cyber-physical systems (CPS), with diverse applications including, but not limited to, vehicles, space technologies, healthcare devices, and smart buildings. Software bugs in these systems can lead to significant consequences, ranging from substantial financial losses to potential threats to human safety. Formal verification is the only known method capable of mitigating such bugs with strong guarantees, making it a crucial step to developing bug-free CPS. This report showcases three distinct works in the field of formal methods â Verbatim++, a verified, performance-optimized, and semantically rich lexer; Lean4, an interactive theorem prover, and a functional programming language; and seL4, a general-purpose operating system kernel that has been completely verified. These works present a range of methods and potential avenues for formal verification within CPS. Additionally, the report exposes some of the required modifications to current methods to fit the unique requirements of CPS.
Background papers
Exam president: Prof. George Candea
Thesis advisor: Prof. Viktor Kuncak
Co-examiner: Prof. Clément Pet-Claudel
Abstract
The software has extended its reach into cyber-physical systems (CPS), with diverse applications including, but not limited to, vehicles, space technologies, healthcare devices, and smart buildings. Software bugs in these systems can lead to significant consequences, ranging from substantial financial losses to potential threats to human safety. Formal verification is the only known method capable of mitigating such bugs with strong guarantees, making it a crucial step to developing bug-free CPS. This report showcases three distinct works in the field of formal methods â Verbatim++, a verified, performance-optimized, and semantically rich lexer; Lean4, an interactive theorem prover, and a functional programming language; and seL4, a general-purpose operating system kernel that has been completely verified. These works present a range of methods and potential avenues for formal verification within CPS. Additionally, the report exposes some of the required modifications to current methods to fit the unique requirements of CPS.
Background papers
- Verbatim++: verified, optimized, and semantically rich lexing with derivatives https://dl.acm.org/doi/abs/10.1145/3497775.3503694
- seL4: formal verification of an OS kernel https://dl.acm.org/doi/10.1145/1629575.1629596
- The Lean 4 Theorem Prover and Programming Language (System Description) https://doi.org/10.1007/978-3-030-79876-5_37
Practical information
- General public
- Free
Contact
- edic@epfl.ch