Note:

The following publications are related to a newly emerging technology that combines a  light weight formal methods approach and Java in statically analyzing Java source code and verifying its partial correctness.

Keywords: static analysis, verification, Java, Object-Oriented, theorem proving, formal methods. All papers have been presented to the conferences below.

Refereed Publications:

·         Applying an Invariant Based Approach to Detecting Illegal Array Bounds in Java.
Proceedings of the 4th International Conference on Systemics, Cybernetics and Informatics (to appear), July 2000, Orlando, FL

·         A Formal Methods Based Static Analysis Approach for Detecting Runtime Errors in Java Programs. Accepted at  the ECOOP 2000 Workshop on  Formal Techniques for Java Programs.  Proceedings of ECOOP2000  Fernuniversitaet Hagen (to appear). June 2000, Sophia-Antipolis, France

·         A Generic Approach of Static Analysis for Detecting Runtime Exceptions in Java Programs. Published in the Proceedings of the 23rd Annual IEEE International Computer Software and Application Conference (COMPSAC'99). October 1999, Phoenix, AZ, pp.67.

·         Detecting Null Pointer Violations in Java Programs. Published in proceedings of  the 23rd Annual IEEE International Computer Software and Application Conference (COMPSAC'99). October 1999, Phoenix, AZ, pp.456.

·         Applying Static Analysis for Detecting Null Pointers in Java Programs. Published in the proceedings of  the 5th International Conference on Information Systems Analysis and Synthesis (ISAS'99). August 1999, Orlando, FL.

·         Code Synthesis based on Object Oriented Design Models and Formal Specifications. Published in the Proceedings of the 22nd Annual IEEE International Computer Software and Application Conference (COMPSAC'98). August 1998, Vienna, Austria, pp. 390­396.

 

 

Technical Reports

 

·         A Light-Weight Approach to Applying Formal Methods in Software Development.  Ph.D dissertation and technical report. Depaul University, June 1999

·         Using a Light­Weight Theorem Prover in Code Synthesis and Optimization from Formal Specifications. A prototype has been developed.

·         Venus: A User's Guide. DePaul ISE Internet Z archive, August 1998. Available via the web at http://saturn.cs.depaul.edu/~fm.

·         Venus: A C++ Code Generation Tool. A White Paper, August 1997. Available via the web at http://saturn.cs.depaul.edu/~fm.

·         A Light­Weight Approach to Formal Methods. Published in the Proceedings of the Software Engineering Symposium, DePaul University. May 1997, Chicago, IL.

·         Detecting Array Index Out of Bounds Violations in Java Programs. Published in the Proceedings of the Software Engineering Symposium, DePaul University. May 1998, Chicago, IL.