This directory contains files for Technical Report CSRG-396, entitled
"Lightweight Reasoning About Program Correctness" by Marsha Chechik
and Wei Ding.

The contents of the directory are as follows:

0) README       (1 KB -- the ASCII file you are currently reading)
1) tr396.ps	(523 KB -- the PostScript version of the report)
2) tr396.ps.gz	(76 KB -- the PostScript compressed with "gzip")

If you have the UNIX "gunzip" program, get the file "tr396.ps.gz".
Remember to transfer the file in binary mode.  After the transfer, use
"gunzip" to extract the original document, then print it on a
PostScript printer.

If  you do not have  either of the programs  above, get the file "tr396.ps" in
ASCII mode and print it on a PostScript printer.

Should you have any questions or comments about  this technical report, please
contact	 chechik@cs.toronto.edu.



Lightweight Reasoning about Program Correctness

Marsha Chechik    and       Wei Ding
November 1999


Automated verification tools vary widely in the types of properties
they are able to analyze, the complexity of their algorithms, and the
amount of necessary user involvement.  In this paper we propose a
framework for step-wise automatic verification and describe a
lightweight scalable program analysis tool that combines abstraction
and model checking.  The tool guarantees that its \emph{True} and
\emph{False} answers are sound with respect to the original system.
We also check the effectiveness of the tool on an implementation of
the Safety-Injection System.