Two source directories are delivered with each Kiasan invariant object.

Kiasan-Red-Black-Tree-src  Contains the original source used by the KSU group
                           which can be used with Kiasan/Sireum software 
                           analysis platform libraries located at
                             http://code.google.com/p/sireum/

Red-Black-Tree-src         Contains source files that have no dependency on
                           Kiasan/Sireum libraries with annotations of the
                           contract specifications in JML (as comments).
                           No tools currently can process these JML
                           specification directly.  You would need to use these
                           JML contract specs as guidance in forming your
                           own analysis tool-specific contract specs.

