BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Formal methods for software-controlled cyber-physical systems
DTSTART:20230706T140000
DTEND:20230706T160000
DTSTAMP:20260406T190013Z
UID:c0203f5c48a72dc65869a2235eaf8698af5dbb2a0f2f632fd07212d1
CATEGORIES:Conferences - Seminars
DESCRIPTION:Samuel Chassot\nEDIC candidacy exam\nExam president: Prof. Geo
 rge Candea\nThesis advisor: Prof. Viktor Kuncak\nCo-examiner: Prof. Cléme
 nt Pet-Claudel\n\nAbstract\nThe software has extended its reach into cyber
 -physical systems (CPS)\, with diverse applications including\, but not li
 mited to\, vehicles\, space technologies\, healthcare devices\, and smart 
 buildings. Software bugs in these systems can lead to significant conseque
 nces\, ranging from substantial financial losses to potential threats to h
 uman safety. Formal verification is the only known method capable of mitig
 ating such bugs with strong guarantees\, making it a crucial step to devel
 oping bug-free CPS. This report showcases three distinct works in the fiel
 d of formal methods – Verbatim++\, a verified\, performance-optimized
 \, and semantically rich lexer\; Lean4\, an interactive theorem prover\, a
 nd a functional programming language\; and seL4\, a general-purpose operat
 ing 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.\n\nBackground paper
 s\n\n	Verbatim++: verified\, optimized\, and semantically rich lexing with
  derivatives https://dl.acm.org/doi/abs/10.1145/3497775.3503694 \n	seL4: f
 ormal verification of an OS kernel https://dl.acm.org/doi/10.1145/1629575
 .1629596\n	The Lean 4 Theorem Prover and Programming Language (System Desc
 ription) https://doi.org/10.1007/978-3-030-79876-5_37\n
LOCATION:INN 326 https://plan.epfl.ch/?room==INN%20326
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR