This is a partial list of researchware prototyping Ajay Chander's scientific work.

[1997] MiniCoq: A novel extension to the Coq program verification tool to support efficient proof verification in the manner of proof-carrying code.  Software and technology are described in a few international presentations, such as http://web.comlab.ox.ac.uk/oucl/strachey/huet-ht98.html

[2003] PHAT: A Provable High Assurance Trust Management Kernel.  A high-assurance access control system, with support for delegation that is built entirely from the formal methods tool PVS.  Described in the following papers:

Ajay Chander, Drew Dean, and John C. Mitchell. Reconstructing Trust Management.  Journal of Computer Security, Volume 12, Issue 1, IOS Press, pp 131-164, 2004.

Ajay Chander, Drew Dean, and John C. Mitchell.  A Distributed High Assurance Reference Monitor. In Proceedings of the 7^th International Conference on Computer Security, September 2004, Springer LNCS 3225, pp 231-244.

[2005] JVer: A Java Verifier.  A program for analyzing Java bytecode for security.  Includes several novel research work, described in the following papers and patents:

Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, and George Necula.  JVer: A Java Verifier. In Proceedings of the Conference on Computer Aided Verification (CAV'05), July 2005.

Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, and George Necula.  Enforcing Resource Bounds via Static Verification of Dynamic Checks. In Proceedings of the European Symposium on Programming (ESOP'05), Lecture Notes in Computer Science, Volume 3444, March 2005, pp 311 – 325.

Ajay Chander, Nayeem Islam, David Espinosa, George Necula, and Peter Lee.  Performing Checks on the Resource Usage of Computer Programs.  Patent pending.

Ajay Chander, Nayeem Islam, David Espinosa, Peter Lee, and George Necula.  Method and Apparatus for Analyzing and Limiting Resource Use of Sequential Computer Programs.  Patent pending.