Dear all, I was using PVS and looking for PVS formalizations of the following C datatypes :-> 1. pointer 2. struct 3. array 4. union 5. double 6. float 7. char 8. int If some one can direct me to already built libraries that give such formalizations, then it will be very helpful to me. thanks and regards, _______________ Navneet Kataria