# Examples

Here you can download some examples running on **LEAP**. The examples include concurrent and sequential programs.

## Safety Verification for Concurrent Programs

The concurrent examples for safety verification include:

- An implementation of a concurrent lock-coupling single-linked lists. More information regarding this example can be found on this paper.
- An implementation of a coarse-grained unbounded concurrent queue
- A lock-free stack implementation
- An implementation of a lock-free non-blocking queue
- A simple mutual exclusion algorithm based on tickets implemented with integers.
- A simple mutual exclusion algorithm based on tickets implemented with sets of integers.

title | description |
---|---|

list | Concurrent lock-coupling single-linked lists |

unbounded-queue | Concurrent coarse-grained lock-based unbounded queues |

lock-free stack | Concurrent lock-free stacks |

lock-free queue | Concurrent lock-free non-blocking queues |

ticketint | Mutual exclusion algorithm based on tickets using integers |

ticketset | Mutual exclusion algorithm based on tickets using sets |

## Safety Verification for Sequential Programs

The sequential examples for safety verification include:

- An implementation of skiplists with an unbounded number of levels. More information regarding this example can be found on this paper.
- A skiplist implementation which is part of the open-source project KDE.
- A bunch of examples dealing with skiplists of a fixed number of levels. More information about this example can be found on this paper

title | description |
---|---|

skiplist | Skiplists of unbounded number of levels |

skiplist-kde | Skiplist implementation from the open-source project KDE |

skiplist_1 | Skiplists of at most 1 level |

skiplist_2 | Skiplists of at most 2 levels |

skiplist_3 | Skiplists of at most 3 levels |

skiplist_4 | Skiplists of at most 4 levels |

skiplist_5 | Skiplists of at most 5 levels |

## Liveness Verification for Concurrent Programs

The concurrent examples for liveness verification include:

- A simple mutual exclusion algorithm based on tickets implemented with sets of integers.

title | description |
---|---|

ticketset | Mutual exclusion algorithm based on tickets using sets |

list | Concurrent lock-coupling lists |

## All Examples

Alternatively, you can download all examples in a single zip file from here:

title | description |
---|---|

all examples | All examples in a single zip file |