컨텐츠 시작
학술대회/행사
초록검색
| 제출번호(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 |