Partial Verification of List-Sorting Algorithms

This directory contains examples of sorting programs manipulating singly linked lists of the form

typedef struct node {
   struct node *n;
   int data;
} *L;
The operational semantics is based on the analysis of singly linked lists with extra information for inequality.
There is an extra instrumentation predicate for keeping track of sortedness. For space efficiency reasons this predicate is not an abstraction predicate. More information about the analysis is available in the paper:
"Putting Static Analysis to Work for Verification: A Case Study", Lev-Ami T., Reps T., Sagiv., M. and Wilhelm, R., Appeared in the proceedings of the International Symposium on Software Testing and Analysis (ISSTA) 2002.

List of examples and their descriptions

For faster convergence use the `-join part' option. (See additional comments below.)
Example Example description Properties checked Command line
bubbleSort A function that performs bubble sort on a list by swapping list elements.
  1. Absence of null dereferences
  2. Output list is sorted in ascending order
  3. Output list is a permutation of the input list
tvla bubbleSort unsorted
bubbleSort_bug A function that performs bubble sort on a list by swapping list elements.
  1. Absence of null dereferences
  2. Output list is sorted in ascending order
  3. Output list is a permutation of the input list
tvla bubbleSort_bug unsorted
insertSort A function that performs insertion sort on a list.
  1. Absence of null dereferences
  2. Output list is sorted in ascending order
  3. Output list is a permutation of the input list
tvla insertSort unsorted
insertSort_bug1 A function that performs insertion sort on a list.
  1. Absence of null dereferences
  2. Output list is sorted in ascending order
  3. Output list is a permutation of the input list
tvla insertSort_bug1 unsorted
insertSort_bug2 A function that performs insertion sort on a list.
  1. Absence of null dereferences
  2. Output list is sorted in ascending order
  3. Output list is a permutation of the input list
tvla insertSort_bug2 unsorted
merge A function that merges two sorted singly-linked lists into one sorted list.
  1. Absence of null dereferences
  2. Merged list is sorted in ascending order
  3. Merged list contains all elements of the input lists
tvla merge merge
reverse A function that reverses a sorted singly-linked list in-situ.
  1. Absence of null dereferences
  2. Output list is sorted in descending order
tvla insertSort sorted

Comments

The original C functions were pre-processed in the following ways in order to simplify the analysis:
  1. Statements that assign to fields are preceded by statements that assign the value NULL to the fields.
    For example, x->n = y; is replaced with x->n = NULL; x->n = y;
  2. Statements that copy a value from one field to another are simplified by using temporary variables.
    For example, x->n = y->n; is replaced with the sequence of assignments
    t = y->n; x->n = NULL; x->n = t; t = NULL;
Program conditions are modelled by two actions---one for the true branch and one for the false branch.