Semantics with Applications:
	Model-Based Program Analysis

	Hanne Riis Nielson  and  Flemming Nielson

	Computer Science Department, Aarhus University, 
	Denmark, (October 1996) 

These notes on model-based program analysis have been used for teaching
semantics-based program analysis to third year students familiar with
denotational semantics as covered in Chapter 4 of

	H.R.Nielson, F.Nielson:
	Semantics with Applications: A Formal Introduction,
	Wiley, 1992. [ISBN 0 471 92980 8]

(referred to as [NN] in the sequel).  Indeed, these notes may be used
as an alternative to the treatment of static program analysis in
Chapter 5 of [NN]. The present notes go deeper into the ideas behind
program analysis: how to define an analysis, how to prove it correct,
how to implement it, and how to use its results for improving the
program at hand. Furthermore, the main part of the development focuses
on the intuitively understandable analysis of "detection of signs" and
only develops the somewhat more demanding analysis of [NN, Chapter 5]
towards the end.

For a short course (based on Sections 1.2, 1.3, 4.1, 4.2, and 4.3 of
[NN]) we recommend covering just Chapters 1 and 2 of this note.


Aarhus, October 1996                        H.R.Nielson & F.Nielson