This thesis is about methods for establishing semantic properties of programs and
how those methods can be strengthened. Finding (semi-)algorithms for deciding
semantic properties is a non-trivial task and such algorithms will, by necessity,
give approximate answers. This means that for any property of interest, there is
a spectrum of algorithms computing answers to various degrees of precision,
ranging from computationally cheap, low-precision algorithms to expensive,
potentially non-terminating algorithms with very high precision. Finding
approximations precise enough to be useful, and that at the same time make the
algorithms cheap enough, is a real challenge.

In this thesis we consider program analysis and program verification, which are
two approaches  for establishing program properties with contrasting requirements
regarding precision and cost. Program  analysis consists of automatic and
computationally cheap algorithms that terminate for all programs and  whose prime
usage is in situations where runtime is a major factor or where only limited
resources are available. Program verification by deduction based on logic and
theorem proving gives higher precision but  is expensive and have no termination
guarantee. It is often used in situations where it is more costly to  modify the
program than allowing the verification process more time and resources.

Common to these two approaches is the desire to move closer to the middle of the
spectrum of algorithms. For algorithms formulated as program analyses, this means
increasing their precision, and for algorithms formulated as program verifiers,
it means making them terminate without user interaction for a larger set of programs.

The work presented in this thesis can be divided into three parts. The first part
investigates the impact a number of features have on the precision of a type-based
program analysis for Haskell. The results presented, make it easier for a designer
of a type-based program analysis to choose what features to add to the analysis in
order to get sufficiently high precision.

The second part concerns how program verification can be integrated with program
analysis in order to make the verification cheaper and more automatic. We show how
a program analysis can be embedded in the tactic language of a theorem prover to
allow for a close integration of program analysis and verification. We also show,
in particular, how a dependence analysis can be used in a theorem prover for Java
to make the handling of loops more automatic.

The third part concerns how type-based program analysis can be strengthened by
plugging in additional, externally computed information. We do this by presenting
a modular method for parameterizing type-based program analyses over information
about the analyzed program's execution. The parameterization is done in such a way
that a modular proof of correctness is obtained, removing the need to prove
correctness of each instantiation separately. We also show how our method of
parameterization can be used to allow for flow-sensitive heap types by plugging in
alias information.