SFlab

English | 한국어

프로그램 검증 워크숍 2026


2026년 7월 28일–30일

프로그램 검증 워크숍은 CRIS를 중심으로 Rocq, interaction tree, CRIS simulation에서 시작해 Separation Logic과 linked-list 프로그램의 전체 검증까지 다루는 3일 워크숍입니다. 이론 강의와 실습을 병행합니다.

[CRIS 프로젝트 페이지]

행사 정보


일정 및 시간. 2026년 7월 28일–30일, 매일 10:00–18:00.

장소. 서울대학교 138동 컴퓨터연구소 6층 민상렬홀.

오는 길.

  • 서울대입구역(2호선) 3번 출구 → 5511번 버스 → 공동기기원 정류장 하차.
  • 낙성대역(2호선) 4번 출구 → 마을버스 02번 → 공동기기원 정류장 하차.

[공식 오시는 길] [캠퍼스맵]

주최. KAIST PLRG.

주관. 서울대학교 Software Foundations Lab.

온라인 참여. [Zoom 등록] 한 번 등록하면 3일 모두 참여할 수 있으며, 접속 링크는 이메일로 발송됩니다.

Zoom 녹화본(2026년 7월 28일). [1부] [2부]

Zoom 녹화본(2026년 7월 30일). [녹화본] 암호: #u+7n9Rn

CRIS 강의. CRIS: The power of imagination in specification and verification [영상(17:47부터)] [강의자료]

제공. 점심과 커피.


준비

실습 자료. [GitHub 저장소]

CRIS 참고 자료. [CRIS의 interaction tree]

설치. 워크숍 전에 저장소를 clone하고 README의 설치 안내를 따라 실습 자료에서 사용하는 CRIS workshop snapshot을 설치해 주세요. 설치 후 저장소 최상위 디렉터리에서 make check를 실행해 주세요.

AI agent. AI 보조 증명 실습에는 로컬 저장소의 파일을 수정하고 명령을 실행할 수 있는 coding agent 사용을 권장합니다. 권장 선택지는 Codex의 GPT-5.6-Sol, 또는 Claude Code의 Claude Fable 5입니다. Claude Mythos 5 접근 권한이 있다면 해당 모델도 사용할 수 있습니다. 같은 기능을 제공하는 다른 agent도 사용할 수 있습니다.

Coqtail MCP 설치(선택 사항).

Coqtail MCP를 사용하면 Codex나 Claude Code가 실행 중인 Rocq 증명 세션과 상호작용할 수 있습니다. Python 3.10 이상과 PATH에서 실행할 수 있는 Rocq 설치가 필요합니다. 

git clone https://github.com/park-sunho/Coqtail-mcp.git
cd Coqtail-mcp
python3 -m venv .venv
.venv/bin/pip install -e .

설치한 서버를 사용할 agent에 등록합니다:

# Codex
codex mcp add coqtail -- "$PWD/.venv/bin/coqtail-mcp"
codex mcp list

# Claude Code
claude mcp add --transport stdio coqtail -- "$PWD/.venv/bin/coqtail-mcp"
claude mcp list

agent를 재시작한 뒤 /mcp에서 coqtail이 연결되었는지 확인합니다. 자세한 설정은 공식 설치 안내를 참고하세요.

Codex skill(선택 사항). [ConCRIS Codex skills] 저장소에서 재사용 가능한 증명 workflow를 제공합니다. 일부 전문 지침은 workshop snapshot보다 최신 API를 대상으로 하므로, agent가 현재 checkout의 정의를 먼저 확인해야 합니다.

프로그램


매일 점심은 12:00–14:00, 커피는 16:00–16:30에 제공됩니다.

1일차 — 7월 28일 화요일

Separation Logic 없이 배우는 CRIS 기초

7월 28일 화요일 프로그램
시간 내용
10:00–12:00 이론.
  • Rocq 증명 기초와 interaction tree의 구조 및 event: Ret, Tau, Vis, Choose, Take, IO
  • CRIS module, local state, linking, behavior, simulation, contextual refinement
14:00–16:00 실습.
  • 작은 source/target pair의 simulation case: internal step, local state, observable I/O, nondeterminism
  • abstract key-value map과 strictly sorted mathematical list를 연결하는 representation relation
16:30–18:00 실습.
  • representation relation을 사용한 get과 put function simulation
  • function simulation이 module simulation과 contextual refinement로 이어지는 흐름

2일차 — 7월 29일 수요일

CRIS의 Separation Logic과 Resource Algebra

7월 29일 수요일 프로그램
시간 내용
10:00–12:00 이론. CRIS의 Separation Logic, 메모리 추상화, Resource Algebra.
14:00–16:00 실습. CRIS에서 Separation Logic 증명을 손으로 작성.
16:30–18:00 실습. AI를 활용한 CRIS Separation Logic 증명.

3일차 — 7월 30일 목요일

연결 리스트를 사용한 n번째 소수 프로그램 전체 검증

7월 30일 목요일 프로그램
시간 내용
10:00–12:00 이론. 연결 리스트 기반 n번째 소수 프로그램의 정의와 증명 구조.
14:00–16:00 실습. 프로그램 전체 검증 1부.
16:30–18:00 실습. 프로그램 전체 검증 2부.