SSFT 2025¶
Welcome to the Gillian lab at SSFT 2025!
This lab take the Separation Logic and Compositional Symbolic Execution theory you've seen in the lectures, and recontextualise it with a semi-automatic verification tool built with Gillian.
Installation instructions
See here for installation instructions.
We recommend you follow these ahead of time, as installing the Gillian container can take a while.
Lecture 1: Compositional Software Verification¶
This lecture covers:
Separation logic
Specification and verification of sequential programs for mutating data structures
Tools inspired by separation logic, based on compositional symbolic execution
Lab Session 1: An introduction to Gillian¶
These exercises are in the lab1
directory of the lab repository. They include list algorithms to demonstrate:
Folding and unfolding predicates
Applying proof tactics and lemmas
Calling functions compositionally
Loop invariants
If you have time, check out exercises A-D from the lab2
directory for some examples with different data structures.
Lecture 2: Compositional Symbolic Execution¶
This lecture covers:
- Theoretical foundations - Compositional Symbolic Execution (CSE) and bi-abduction
CSE for a simple C-like state
State-parametric CSE
Functional compositionality
State combinators for CSE
Lab session 2: Further experience with Gillian¶
These exercises are in the lab1
directory of the lab repository. They include:
Some fun, harder examples of data-structure algorithms
List algorithms ported from the real-world Collections-C library
Some harder iterative list algorithms
Feel free to tackle these in any order, and refer back to the Lab 1 exercises if you need a refresher.
At the end of the lab session, we'd hugely appreciate it if you could fill out this survey to help us evaluate Gillian's user experience.
Misc. lab notes¶
The language server highlights compilation errors (and other unexpect problems) in red, and verification falures in blue.
The debugger supports breakpoints! This can be handy when restarting the debugger after making changes to your code; assign breakpoints to the relevant lines and click the Continue button
.
- If you get a
SIGPIPE
or"Broken pipe"
error, try making a small change to your code and trying again. Note from Nat: I have *absolutely no idea* why this happens. Even with a repro, it disappears if I try to track it down 🙃
- If you get a
If Gillian seems stuck or unresponsive, or if the WISL language server fails to start, try opening the Command Palette with (
F1
orCtrl+Shift+P
by default) and running the "Reload window" command.A version of the Gillian VSCode extension built for older versions of VSCode (1.92.0) can be found
here
; your mileage may vary.