Programs

Below is a list of heap-manipulating programs, verified using GBT.

Example	Description	Model File	Graphical Model	Result Patterns
flatten	Flattening of a list-of-lists	.tgz file
concat	PALE singly-linked list concatenation	.tgz file
fumble	PALE singly-linked list fumble	.tgz file
walk	PALE singly-linked list walk	.tgz file
reverse	PALE singly-linked list reversal	.tgz file

Protocols

Example	Description	Model File	Graphical Model	Result Patterns
DYMO draft 10
- interm. reply	GBT model of the DYMO ad hoc routing protocol draft version 10. Full model, i.e., intermediate nodes may also reply to RREQs if they have a fresh enough route.)	.tgz file
- dest. reply	Alternative model, in which only the target node may reply to an RREQ	.tgz file	pdf	pdf
DYMO draft 05
	GBT model of the DYMO ad hoc routing protocol draft version 05.	.tgz file
Public/private servers I
	GBT model of (a variant of) the "Public/private servers I" example used by König and Kozioura	.tgz file
Public/private servers II
	GBT model of (a variant of) the "Public/private servers II" example used by König and Kozioura	.tgz file
Firewall I
	GBT model of (a variant of) the "Firewall I" example used by König and Kozioura	.tgz file
Firewall II
	GBT model of (a variant of) the "Firewall II" example used by König and Kozioura	.tgz file