Verification of Second-Order Functional Programs

• Main Author: Aderhold, Markus Axel
• Format: Others
• Language: English; en
• Published: 2009
• Online Access: https://tuprints.ulb.tu-darmstadt.de/1865/1/Dissertation-Aderhold_final_sw.pdf; Aderhold, Markus Axel <http://tuprints.ulb.tu-darmstadt.de/view/person/Aderhold=3AMarkus_Axel=3A=3A.html> (2009): Verification of Second-Order Functional Programs.Darmstadt, Technische Universität, [Ph.D. Thesis]

Functional programming languages such as Haskell or ML allow the programmer to implement and to use higher-order procedures. A higher-order procedure gets a function as argument and applies this function to some values. For instance, procedure 'map' applies a function to all elements of a list and returns the list of the result values. Verifying that a higher-order program satisfies a certain property is particularly challenging, because it involves reasoning about indirect function calls; for instance, a call 'map(f, l)' directly calls procedure 'map' and indirectly calls function 'f' if list 'l' is non-empty. Using a higher-order procedure 'g', a procedure 'f' can be defined by higher-order recursion; i. e., procedure 'f' (directly) calls 'g' and passes itself as an argument to 'g', which leads to indirect recursive calls. These indirect recursive calls make reasoning about higher-order programs difficult. In this thesis we show how the verification of second-order functional programs can be supported by semi-automated theorem provers. 'Second-order' means that a procedure such as 'map' may only be applied to a first-order function, not to a higher-order function. This suffices for most examples that occur in practice and has advantages concerning the semantics of programs. Our goal is to verify the total correctness of programs. This requires a proof that the program terminates and that the result of the computation satisfies a user-defined property. Consequently, we investigate two main problems: termination analysis and inductive theorem proving. The general contribution of this thesis is the automated analysis of the dynamic call structure in second-order programs (introduced by indirect function calls). Specifically, we describe a technique that automatically analyzes and proves termination of many procedures that occur in practice and a technique that automatically synthesizes induction axioms that are suitable to prove properties of these procedures by induction. Finally, we show how the proof of the base and step cases can be supported by an automated theorem prover. The techniques have been implemented in the verification tool VeriFun. Several case studies confirm that they work well in practice and provide a significantly higher degree of automation than other inductive theorem provers.