Automating inductive reasoning with recursive functions

Abstract

Formally ensuring software reliability is challenging due to the growing complexity of software in terms of its size, used unbounded and inductive data types and supported workflow. As manual code analysis is not a viable solution, automated reasoning approaches are needed for proving software correct. There are several prominent methods addressing this challenge by (i) translating parts of a system to a logic-based formalism and (ii) using automated theorem proving to validate certain safety and liveness program properties.In this context a vital ingredient in automated reasoning is inductive reasoning, which can/must be used whenever repetition is present in a software component, e.g. loops or recursive data structures in computer programs or feedback loops in electric circuits. The two main branches in the literature are explicit and implicit induction. In this thesis focus on the former approach which is based broadly on the Noetherian well-founded induction principle. There is a plethora of research already done in this area with several automated theorem provers as well as proof assistants are equipped with inductive reasoning techniques. Some of the earliest ones are Nqthm/ACL2, Inka and Oyster/CLAM. Recently, modern automated theorem provers, such as ZipperPosition, CVC4 and Vampire, started to incorporate inductive types and reasoning.The aim of the proposed thesis is to advance the state-of-the art in inductive reasoning within first-order logic theorem proving, by using automating reasoning with recursive function definitions over inductive data types.