TVLA Examples
This directory contains examples of the following TVLA specifications:
- ambient : Verifying partial correctness of mobile code.
- concurrent : Verifying partial correctness of various concurrent algorithms.
- dll : Verifying partial correctness of programs manipulating acyclic doubly-linked lists.
- gc : Verifying partial correctness of a simple mark-and-sweep garbage collector.
- sll : Verifying partial correctness of programs manipulating acyclic singly-linked lists.
(These examples use the Differencing feature to automatically generate update formulae.)
- sll/sll_cyclic :
Verifying partial correctness of program manipulating possibly cyclic singly-linked lists.
- sll_sorting : Verifying partial correctness of list-sorting algorithms.
- tree : Verifying partial correctness of tree-manipulating programs.
Comment: After analysis finishes, the figure
``Total number of messages'' indicates how many abstract configurations
have triggered an error message. Total number of messages=0 means that
the program was successfuly verified against the specified properties.