Here (in reverse cronological order) are some PhD theses whose authors made use of PVS:

• Java Program Verification in Higher-Order Logic with PVS and Isabelle
  Marieke Huisman, University of Nijmegen, The Netherlands, 2001.

• Systematic Verification of Pipelined Microprocessors
  Ravi Hosabettu, University of Utah, 2000.

• Formal Software Development using Generic Development Steps
  Axel Dold, UniversitŠt Ulm, Germany, 2000.

• Real-Time Reactive System Development - A Formal Approach Based on UML and PVS
  Darmalingum Muthiayen, Concordia University, 2000.
  Available by request to d_muthi@cs.concordia.ca

• Mechanical Verification of Compiler Correctness
  David Stringer-Calvert, University of York, 1998.

• Object Code Verification
  Matthew Wahab, University of Warwick, 1998.

• Computer Assisted Analysis of Multiprocessor Memory Systems
  Seungjoon Park, Department of Electrical Engineering, Stanford University, June 1996.

• Compositional Verification of Parallel Programs using Epistemic Logic and Abstract Assertional Languages
  Marten van Hulst, University of Utrecht, 1995. (separate title page)

• Transformations on Dependency Graphs: Formal Specification and Efficient Mechanical Verification
  Sreeranga Rajan, University of British Columbia, 1995.

• A Verification Assistant for a Real-Time Logic
  Jens Skakkebaek, Technical University of Denmark, 1994.