In this page we describe the experiments performed to determine how precise is a neural network trained with our approach, in classifying actually valid and invalid objects generated using the Korat tool.

Running the experiments

To generate a classifier that will approximate the class invariant of, let's say Singly Sorted List with scope 6, you can run the corresponding script from the folder data-structures:

./experiments/koratstructs/validate-approach-singlysortedlist-scope6.sh

First, the script will create the training set, that is the positive instances created using the data structure builders, and then the negative instances created using our approach. After that, the script will train a neural network that will be evaluated using instances generated with Korat as the validation set.

In the evaluation step we measure precision and recall in classifying positives (negatives) of the validation set. Precision means how many of the objects classified as positives (negatives) are actually positives (negatives)? While recall means how many of the actually positives (negatives) objects were classified as positives (negatives)? While higher these values are, better is our classification accuracy:

Results of our approach

The following table shows the precision and recall obtained from running each script with name validate-approach-*.sh

For each scope k we report:

The total positive (+) and negative (-) instances generated to train the neural network.

ft: the total features (positions in the input vector).

hlu: the hidden layer units, determined through parameter optimization.

pst(sec): the time in which the parameters search was performed, in seconds.

tt(sec): the training time, in seconds.

tp: true positives (instances that should be classified as positives and are classified as positives)

fp: false positives (instances that should be classified as negatives but are classified as positives)

tn: true negatives (instances that should be classified as negatives and are classified as negatives)

fn: false negatvies (instance that should be classfied as negatives but are classified as positives)

Using this last four values, we calculate and report the precision and recall for the positives and negatives instances.

Results of the Daikon approach

We also generated likely invariants using the Daikon tool and performed the same measure that in our approach. The generated invariants can be seen in the corresponding classes in the folder data-structures/src/main/java/koratstructures. To evaluate the Daikon invariant in Singly Sorted List with scope 6 you can execute the following command from the root directory:

java -cp lib/korat.jar RunDaikonRepOK SortedList instancesapproachvalidation/ssllpos6.obj instancesapproachvalidation/ssllneg6.obj

To run the invariant for Singly Sorted List with the other scopes, you can use the files of the form instancesapproachvalidation/ssllpos*.obj for the positives and instancesapproachvalidation/ssllneg*.obj for the negatives.

For the rest of the case studies use the following parameters:

SinglyLinkedList:

SinglyLinkedList instancesapproachvalidation/sllpos*.obj instancesapproachvalidation/sllneg*.obj

DoublyLinkedList:

DoublyLinkedList instancesapproachvalidation/dllpos*.obj instancesapproachvalidation/dllneg*.obj 

BinaryTree:

BinaryTree instancesapproachvalidation/btpos*.obj instancesapproachvalidation/btneg*.obj

BinarySearchTree:

SearchTree instancesapproachvalidation/bstpos*.obj instancesapproachvalidation/bstneg*.obj

RedBlackTree:

RedBlackTree instancesapproachvalidation/rbtpos*.obj instancesapproachvalidation/rbtneg*.obj

BinomialHeap:

BinomialHeap instancesapproachvalidation/bhpos*.obj instancesapproachvalidation/bhneg*.obj

The results can be seen in the following table: