- 다음글엣지인공지능 22.09.01
연구
연구실
정형 컴퓨팅 및 인공지능연구실 인공지능시스템
Formal Computing and AI Lab
담당교수 김지응
제4공학관 D724호
연구실 소개
우리 연구실은 프로그래밍 언어 이론과 소프트웨어 공학에서 사용되는 기술들을 활용하여 시스템 소프트웨어와 신경망과 같은 핵심 컴퓨팅 구성 요소의 신뢰성을 향상시키기 위한 연구들을 수행 중 입니다. 특히, 우리의 작업은 정형 검증(formal verification)-수학 및 논리를 통하여 증명 대상의 무결성을 보장하는 방법-에 중점을 두고 있습니다. 정형 검증은 매우 비용이 큽니다. 따라서 우리는 분해(decomposition)와 추상화(abstraction)를 통해 이를 더욱 확장 가능하고 효과적으로 만드는 데 중점을 두고 있습니다. 본 연구실은 해당 연구의 결과를 실제 운영 체제(OS)와 분산 시스템에 적용하였으며 이를 통해 정형 검증 연구에 중요한 성과들을 발표 하였습니다. 또한, 현재는 인공 신경망에 대한 효율적인 정형 검증 방법론 연구를 활발히 수행 중 입니다.
연구분야
프로그래밍 언어 이론 정형 검증 시스템 소프트웨어 신뢰성 인공신경망 신뢰성대표 논문
- Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Zhong Shao: AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. Proc. ACM Program. Lang. 8(OOPSLA1): 419-448 (2024)
- Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, Zhong Shao: LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. Proc. ACM Program. Lang. 8(PLDI): 1140-1164 (2024)
- Jieung Kim, Ronghui Gu, Zhong Shao: SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification, Journal of Systems Architecture. 147: 103049 (2024)
- Wolf Honoré*, Jieung Kim*, Ji-Yong Shin, Zhong Shao: Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems (* equally contributed) Proc. ACM Program. Lang. 5(OOPSLA): 1-31 (2021)
- Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro: Certified concurrent abstraction layers. PLDI 2018
- Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, David Costanzo: CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. OSDI 2016