Title: Automating inductive reasoning with recursive functions
Language: English
Authors: Hajdu, Marton 
Qualification level: Diploma
Advisor: Kovacs, Laura 
Issue Date: 2021
Number of Pages: 101
Qualification level: Diploma
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.
Keywords: formal methods; inductive reasoning; first-order theorem proving; induction
URI: https://doi.org/10.34726/hss.2021.84140
http://hdl.handle.net/20.500.12708/17065
DOI: 10.34726/hss.2021.84140
Library ID: AC16168885
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

23
checked on Jun 3, 2021

Download(s)

25
checked on Jun 3, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.