Paul Y Gloess
LaBRI
(under construction)
Research (Equipe MVTsi):
Imperative Programming
in PVS
Miscellaneous PVS applications
Formalizing ASN.1 Semantics
Timed Automata
Mechanizing Géraud Sénizergues proof of "L(A)=L(B) decidable ..." in PVS
Teaching and administration
(
E.N.S.E.R.B.
)
© Copyright 1999-2000
Paul Y Gloess