• Proof assistant library (mainly about PVS);
• some Bordeaux PVS applications (warning: old site, many bad links, most recent PVS dumps are available at ENSEIRB);
• PVS imperative program verification (warning: site is in reconstruction after relocation, many bad links);
• PVS imperative program verification summary (new);
• Fixpoint theory and PVS inductive sets;
• A PVS theory of well founded recursion;
• Alose semantics, a class project from 2001--2002 to 2002--2003
• Alose (Automatisation de LOgigrammes de Sécurité), développé par Kaninda Musumbu et coll.: slide presentation;
• Alose PVS declarative and operational semantics - 2002--2003 class project results;
• Alose PVS declarative (fixpoint) semantics - 2001--2002 class project results;
• Alose fixpoint semantics 2 december 2002 hand written proofs;
• book available from ENSEIRB library:
The Foundations of Program Verification
Second Edition
Jacques Loeckx and Kurt Sieber
Wiley - Teubner Series in Computer Science

© Copyright 2001-3000 Paul Y Gloess