{'fraction_non_alphanumeric': 0.01736881005173688, 'fraction_numerical': 0.0, 'mean_word_length': 4.698947368421052, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Combining and Strengthening Program Analysis and Verification

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. 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 verifi- 
cation. 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.