This thesis is concerned with analysis of programs. Analysis of programs can be
divided into two camps: static analysis and formal verification.
Static program analyses compute a result and terminate for all programs. Since
virtually all interesting semantic properties are undecidable, a static program
analysis needs to be approximative to ensure termination. When designing such an
analysis it can be hard to know which features that have the largest impact on
the precision and should be added. This is the subject of the first paper in this
thesis in which we investigate the impact a number of features have on the
precision of usage analysis.
Formal verification often refers to deductive verification based on logic and
theorem proving. When verifying a property, the program and the property are both
translated into logical formulas and a theorem prover is used to show that the
property holds for the program. Formal verification is a much more precise and
general purpose technique than static analysis. This does, however, not come for
free. It is extremely hard to find good heuristics for guiding the automatic
construction of proofs. Therefore, user interaction is often required which makes
the verification very time consuming and expensive.
Static program analysis is limited by its approximative nature and program
verification by its high cost. It is, therefore, interesting to try to combine the
strengths of the two techniques. This can be done in both directions: by letting a
static program analysis use a theorem prover designed for program verification or
letting a program verifier use a static program analysis. The latter combination is
the subject of the second and third paper in this thesis.
We make the following contributions:
* We investigate the impact of a number of features on the precision of usage
analysis.
* We show how a static program analysis can be embedded into a theorem prover.
* We show how interactive techniques for handling loops can sometimes be made
automatic by using a dependence analysis.