Verisoft is a long-term research project whose main goal is the
formal verification of a complete computer system. The computer system ---
called the Academic system --- basically consists of hardware, an
operating system and user applications. User programs are written in a
high level programming language, a compiler for which is being verified in
the frame of the project. Together
with a compiler several libraries which implement basic data structures
and algorithms on them are provided. The talk gives an overview of the
formal framework and methods involded in the verification of such
libraries. The application of methods is illustrated by the data structure
for strings example.