The three topics that I am offering are all related to the problem
   of verifying correctness of compilers.

   1. PCC techniques applied to compiled code verification: Recent
      times have seen a shift from compiler verification to compiled
      code verification. Instead of the original aim of verifying
      that a compiler will correctly compile any program that might be
      given to it, we now try to verify that the compiler has
      correctly compiled a program that has been given to it.
      This appears to be an easier problem to solve.

      This study will look at the extent to which PCC based
      techniques have been useful in compiled code verification.

   2 and 3. Since one of the goals of PCC based methods is that the
      resulting system should be fully automated, theorem provers are
      naturally an integral part of the system. We shall study two
      popular theorem provers  PVS and HOL.