허충길 연구실

본 아티팩트는 소프트웨어 검증을 위한 CRIS 논문을 동반하며, 전체 프로젝트 소스 코드와 x86_64 및 arm64 아키텍처용 두 개의 사전 구축된 Docker 이미지를 포함합니다.

본 아티팩트는 소프트웨어 검증 논문 'CRIS: The Power of Imagination in Software Verification'을 동반하며, 전체 프로젝트 소스 코드와 x86_64 및 arm64용 두 개의 사전 구축된 Docker 이미지를 포함합니다.

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

본 논문은 동시성 분리 논리(CSL)의 생존성(liveness) 검증 한계를 극복하기 위해 Lilo를 제안합니다. Lilo는 비국소적 선형화 지점을 가진 동시 객체 검증, 무한 반복 성질 추론, 그리고 모듈식 검증을 지원하는 고차 관계형 CSL입니다. 계층화된 명제(stratified propositions) 기법을 통해 단계 인덱싱 없이 고차 추론을 가능하게 하며, 제거 스택의 종료 보장 검증 등 사례 연구를 통해 확장성을 입증합니다.

본 논문은 수학의 허수 개념을 프로그램 검증에 적용한 CRIS(Contextual Refinement with Imaginary Specification)를 제안합니다. 허수 명세를 통해 분리 논리와 프로그램 정제라는 두 가지 검증 접근법을 통합하며, 증명 분해를 통한 단순화와 IO 이벤트 및 논리적 원자성 같은 복잡한 성질의 우아한 표현을 가능하게 합니다.