컨텐츠 시작
학술대회/행사
초록검색
제출번호(No.) | 0152 |
---|---|
분류(Section) | Special Session |
분과(Session) | (SS-04) Mathematical Logic and Its Applications (SS-04) |
발표시간(Time) | 19th-B-13:30 -- 14:00 |
영문제목 (Title(Eng.)) |
Lessons learned from verifying real-world systems software using separation logic |
저자(Author(s)) |
Jeehoon Kang1 KAIST1 |
초록본문(Abstract) | Recent innovations in separation logic have enabled its use for verifying software that manages memory explicitly, including the use of pointers. However, there are still numerous challenges in verifying real-world systems software such as operating systems and web browsers. Over the past few years, my collaborators, students, and I have expanded the application of separation logic to more real-world features of systems software, including weak-memory concurrency and garbage collection. In this talk, I will share several lessons learned from this endeavor, including: (1) the design of proof constructs should be inspired by algebraic structures, which allows (2) the tedious aspects of the proofs to be easily automated. |
분류기호 (MSC number(s)) |
03B70, 68N15 |
키워드(Keyword(s)) | Separation logic, weak memory, automation |
강연 형태 (Language of Session (Talk)) |
English |