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.

Online participation. [Zoom registration] Register once for all three days. Zoom will send the join link by email.

Zoom recording (July 28, 2026). [Part 1] [Part 2]

Zoom recording (July 30, 2026). [Recording] Passcode: #u+7n9Rn

CRIS lecture. CRIS: The power of imagination in specification and verification [Video (starts at 17:47)] [Slides]

Provided. Lunch and coffee.


Preparation

Workshop materials. [GitHub repository]

CRIS reference. [Interaction trees in CRIS (Korean)]

Installation. Before the workshop, clone the repository and follow the README installation instructions. These pin the CRIS workshop snapshot used by the materials. 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.

Coqtail MCP setup (optional).

Coqtail MCP lets Codex or Claude Code interact with a live Rocq proof session. It requires Python 3.10 or later and a working Rocq installation on PATH. 

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

Register the installed server with your 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

Restart the agent, then use /mcp to check that coqtail is connected. See the upstream installation guide for configuration details.

Optional Codex skills. [ConCRIS Codex skills] provide reusable proof-engineering workflows. Some specialized rules target APIs newer than the workshop snapshot, so the agent should inspect the checked-out definitions before applying them.

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.