[Abstract]
large-scale system software is hard to get right. Especially when concurrency comes in, a number (usually unbounded) of arbitrary interactions and interleaved executions among all system components become easily intractable. However, this complex feature is prevalent in critical software (e.g., OS, Distributed systems) these days, so showing the correctness of these software is important. In this sense, applying formal verification to them is desirable. We propose concurrent certified abstraction layer (CCAL), a modular verification framework that dramatically reduces the high cost of software formal verification. Also, to show its applicability, we verify CertiKOS (an extensible OS & hypervisor with 6100 C and 400 Asm) and WormSpace (a generic distributed system building API with 1000 C). We also propose a novel, compositional, Atomic Distributed Object (ADO) model, which covers multiple strongly consistent distributed systems such as Paxos, Raft, Chain replication and their variances.

[Biography]

Jieung Kim is an assistant professor in the Department of Computer Engineering, Inha university. Before that, he was at Google (Google Core ML and Google Research) as a Research Engineer, mostly working on pKVM formal verification. He obtained his Ph.D. from Yale University, M.S. from KAIST, and B.S from Sungkyunkwan University. During most of his research careers, his main focus was software formal verification.