허충길 연구실

본 논문은 증명 보조기의 제한적인 보호 조건을 극복하기 위해 합성적 이질적 생산성(CHP) 이론 프레임워크를 제시합니다. CHP는 다양한 정의역과 치역 타입을 가진 함수에 적용 가능하며, 합성성을 통해 복합 함수의 생산성을 체계적으로 계산합니다. 이를 기반으로 Rocq용 Coco 라이브러리를 개발하여 생산성 계산과 고정점 생성의 자동화를 제공합니다.

본 논문은 Isabelle/HOL에서 Interaction Trees(ITrees)를 기계화하여 모델 실행과 연역적 검증을 통합하는 프레임워크를 제시합니다. ITrees는 무한 레이블 전이 시스템을 인코딩하면서도 실행 가능한 여구조로, 명령형 프로그램, 메시지 패싱 동시 프로그램(CSP, Circus), 추상 시스템 모델(Z, B)의 검증 도구를 구현합니다. Isabelle 코드 생성기를 통해 모델 애니메이션을 지원합니다.

본 논문은 전이 시스템 간의 행동적 정제를 증명하는 시뮬레이션 방법을 개선합니다. 기존 스터터링 시뮬레이션은 건전성을 보장하기 위해 동기적 진행을 요구하지만, 본 논문은 비동기적 진행만으로도 건전성을 유지할 수 있음을 보입니다. Coq으로 기계화된 FreeSim 기법을 제안하며, CompCert 메타이론 단순화 및 DTrees 라이브러리 개발을 통해 효과성을 입증합니다.

본 논문은 프로그램 순서를 따르는 인-오더 공유 메모리 동시성 모델을 개발하여, 비원자적 접근을 완전히 지원하면서 컴파일러 최적화를 검증합니다. 소스 모델과 중간 표현(IR) 모델의 구분을 통해 매핑의 건전성을 형식적으로 확립하며, 완화된 원자적 접근에 대해서는 로드-스토어 재정렬을 금지합니다. Coq에서 기계화된 증명을 통해 인-오더 소스 모델과 아웃-오브-오더 IR 모델을 형식적으로 연결합니다.

본 논문은 프로그램 검증에서 중요한 공정성(fairness) 속성을 표현하고 추론하기 위한 FOS(Fair Operational Semantics) 이론을 제안합니다. FOS는 임의의 공정성 개념을 운영 의미론으로 표현하며, 분리 논리 기반의 자원 대수를 활용하여 스레드-로컬 추론을 가능하게 합니다. 티켓 락 구현과 약한 메모리 동시성 환경에서의 검증 사례를 통해 스케줄러, 락 구현, 약한 메모리의 공정성을 모두 고려한 추론을 보여주며, 이론과 예제는 Coq으로 완전히 형식화되었습니다.