			>	Session 2
IT304	>	Program Specification and Proof	>	Session 3
			>	Session 4

created by pyg on 15 October 2004, last edition 4 November 2009

Miniproject (Proof assistants)

Mini-project choice, work and questions: 2 new project proposals available.

Finish Ackerman exercise

see Ackerman exercise and Proof Assistant Session 4.

Well founded induction and generalization

PVS inference slides html | pdf (28--31).

Inductive Sets and Fixpoint Induction

PVS inductive sets (or predicates), see PVS language slides html | pdf (28--30) is based upon fixpoint induction, see

Fixpoint theory and PVS inductive set

from document library.

Begin Proof Assistant PVS exercise on inductive sets?

Correctness of a compiler of algebraic expressions into machine code? not done

see compiler in Bordeaux PVS applications (LaBRI page: Warning! Some links are no longer operational);
dump available at ENSEIRB:

~gloess/pvs/2.4/compiler/2.4.compiler.24jan2002.dump.dmp

© Copyright 2001-3000 Paul Y Gloess