Preface

Introduction to Verifiable C    (Verif_sumarray)

Linked lists in Verifiable C    (Verif_reverse)

Stack ADT implemented by linked lists    (Verif_stack)

A client of the stack functions    (Verif_triang)

List segments    (Verif_append1)

Magic wand, partial data structure    (Verif_append2)

String functions    (Verif_strlib)

Functional model of hash tables    (Hashfun)

Correctness proof of hash.c    (Verif_hash)

Introduction to Verified Software Units    (VSU_intro)

VSU specification of the Stack module    (Spec_stack)

VSU specification of the Triang module    (Spec_triang)

Specification of external malloc, free, exit functions    (Spec_stdlib)

VSU verification of the Stack module    (VSU_stack)

VSU verification of the Triang module    (VSU_triang)

Axiomatization of malloc/free/exit    (VSU_stdlib)

linking all the VSUs together with main VSU    (VSU_main)

Malloc/free/exit programmed in C    (VSU_stdlib2)

linking with stdlib2 instead of with stdlib    (VSU_main2)

Postcript and bibliography    (Postscript)

Bibliography    (Bib)