SFlab

English | 한국어

Program Verification Workshop 2026


July 28–30, 2026

The Program Verification Workshop is a three-day workshop on CRIS, progressing from Rocq, interaction trees, and CRIS simulation to Separation Logic and the full verification of a linked-list program. The program combines lectures with hands-on proof development.

[CRIS project page]

Event Information


Date & time. July 28–30, 2026, 10:00–18:00 each day.

Venue. Min Sang-ryeol Hall, 6th floor, Institute of Computer Technology (Building 138), Seoul National University.

Getting there.

  • Seoul Nat'l Univ. Station (Line 2), Exit 3 → Bus 5511 → Joint Instrumentation Center (공동기기원) stop.
  • Nakseongdae Station (Line 2), Exit 4 → Village Bus 02 → Joint Instrumentation Center (공동기기원) stop.

[official directions] [campus map]

Hosted by. KAIST PLRG.

Organized by. Seoul National University Software Foundations Lab.

Participation. Zoom participation and recording are planned.

Provided. Lunch and coffee.


Preparation

Workshop materials. [GitHub repository]

Installation. Before the workshop, clone the repository and follow the README installation instructions. These install the CRIS v2026-07-22 release. Finish by running make check in the repository root.

AI agent. A repository-capable coding agent is recommended for the AI-assisted proof sessions. Recommended options are Codex with GPT-5.6-Sol, or Claude Code with Claude Fable 5. Claude Mythos 5 is also suitable for participants who already have access. Comparable agents that can edit files and run commands in a local repository are also welcome.

Program


Lunch is 12:00–14:00 and coffee is 16:00–16:30 each day.

Day 1 — Tuesday, July 28

CRIS Fundamentals without Separation Logic

Program for Tuesday, July 28
Time Session
10:00–12:00 Theory.
  • Rocq proof basics and interaction tree structure and events: Ret, Tau, Vis, Choose, Take, and IO
  • CRIS modules, local state, linking, behaviors, simulation, and contextual refinement
14:00–16:00 Practice.
  • Simulation cases for small source/target pairs: internal steps, local state, observable I/O, and nondeterminism
  • A representation relation between an abstract key-value map and a strictly sorted mathematical list
16:30–18:00 Practice.
  • get and put function simulations using the representation relation
  • How function simulation leads to module simulation and contextual refinement

Day 2 — Wednesday, July 29

Separation Logic and Resource Algebras in CRIS

Program for Wednesday, July 29
Time Session
10:00–12:00 Theory. Separation Logic, memory abstraction, and Resource Algebras in CRIS.
14:00–16:00 Practice. Separation Logic proofs in CRIS, by hand.
16:30–18:00 Practice. Separation Logic proofs in CRIS with AI assistance.

Day 3 — Thursday, July 30

Full Verification of a Linked-List n-th Prime Program

Program for Thursday, July 30
Time Session
10:00–12:00 Theory. Definitions and proof structure for the linked-list n-th prime program.
14:00–16:00 Practice. Full program verification, Part I.
16:30–18:00 Practice. Full program verification, Part II.