Main techniques:

Type systems
  Topics:
    Universal and Existential Types
    Recursive Types
    Lock types
    Flow-sensitivity
    Subtyping
    Type inference
    Regions
    Linearity

  Cyclone
  Cqual
  Vault
  RCCJava

Dynamic inference
  Daikon

Model Checking
  Topics:
    CTL
    Infinite state transition systems
    Lazy abstraction

  SMV
  Blast

Theorem Proving
  Topics
    Hoare logic
      VCGen
      Weakest preconditions
      Cooperating decision procedures
    Logical Frameworks
      Adequacy
      Canonical forms
      Modeling terms
      Modeling inference rules and proofs
      Modeling meta-theory

  Simplify
  ESC/Java
  Twelf