by Feride Cetin and Kremena Diatchka

Our goal is to verify the implementations in Java of simple data structures using Jahob.

We have implemented some simple data structures in Java, provided specifications for properties they must specify, and attempted to verify that the implementation is correct with respect to these specifications using the verification tool Jahob. We have fully verified the implementations of a singly-linked list with a header node and a queue. All methods of a singly-linked cyclic list, doubly-linked cyclic list and leaf-linked tree also verify, but these classes require further work to ensure the specifications are correct in the initial state of the class. This report presents a brief overview of data structure verification using Jahob, and then continues with a detailed explanation of the specifications we provided. We conclude by summarizing our contributions, commenting on what we have learned, and suggesting directions for future work.

Final report: Data Structure Verification Using Jahob report

Code: Data structures verified with Jahob

Final presentation: Data Structure Verification Using Jahob presentation