The SecJ Secure Information Flow Inferencer developed by former PhD student Qi Sun.
The VERL Verifier for Region Logic developed by former PhD student Stan Rosenberg.