Combining and Strengthening Program Analysis and Verification

This thesis is about methods for establishing semantic properties of programsand how those methods can be strengthened. Finding (semi-)algorithms fordeciding semantic properties is a non-trivial task and such algorithms will, bynecessity, give approximate answers. This means that for any property of interest,there is a spectrum of algorithms computing answers to various degrees ofprecision, ranging from computationally cheap, low-precision algorithms to expensive,potentially non-terminating algorithms with very high precision. Findingapproximations precise enough to be useful, and that at the same time makethe algorithms cheap enough, is a real challenge.In this thesis we consider program analysis and program verification, whichare two approaches for establishing program properties with contrasting requirementsregarding precision and cost. Common to these two approaches is thedesire to move closer to the middle of the spectrum of algorithms. For algorithmsformulated as program analyses, this means increasing their precision, and foralgorithms formulated as program verifiers, it means making them terminatewithout user interaction for a larger set of programs.The work presented in this thesis can be divided into three parts. The firstpart investigates the impact a number of features have on the precision of atype-based program analysis for Haskell. The results presented, make it easierfor a designer of a type-based program analysis to choose what features to addto the analysis in order to get sufficiently high precision.The second part concerns how program verification can be integrated withprogram 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 atheorem 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 ina theorem prover for Java to make the handling of loops more automatic.The third part concerns how type-based program analysis can be strengthenedby plugging in additional, externally computed information. We do this bypresenting a modular method for parameterizing type-based program analysesover information about the analyzed program’s execution. The parameterizationis done in such a way that a modular proof of correctness is obtained, removingthe need to prove correctness of each instantiation separately. We also showhow our method of parameterization can be used to allow for flow-sensitive heaptypes by plugging in alias information