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 참여 및 녹화 예정.

제공. 점심과 커피.


준비

실습 자료. [GitHub 저장소]

설치. 워크숍 전에 저장소를 clone하고 README의 설치 안내를 따라 CRIS v2026-07-22 릴리스를 설치해 주세요. 설치 후 저장소 최상위 디렉터리에서 make check를 실행해 주세요.

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

프로그램


매일 점심은 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부.