Title: Automated Software Verification using Superposition-based Theorem Proving
Other Titles: null
Language: English
Authors: Gleiss, Bernhard 
Qualification level: Doctoral
Keywords: Superposition; Vampire; Software Verification; Semantics; Logic; Theorem Proving; Automated Reasoning
Advisor: Kovacs, Laura 
Issue Date: 2020
Number of Pages: 142
Qualification level: Doctoral
This thesis explores the automated verification of software programs involving loops and arrays using superposition-based theorem proving. It proposes new techniques at the intersection of program semantics, software verification, and automated reasoning. In the first part of the thesis, we introduce an expressive instance of first-order logic modulo theories, called trace logic. We present a sound and complete axiomatic semantics of software programs and use it to capture the partial correctness of program properties as validity statements in trace logic. Our semantics describes each timepoint in the execution of a program uniquely and keeps program locations explicit. We then introduce a verification framework, which handles the inductive reasoning needed in the trace logic domain in order to enable off-the-shelf first-order theorem provers to reason about validity statements in trace logic. Our framework adds instances of an expressive induction axiom scheme explicitly into the search space, in contrast to other approaches which use induction axioms only on the meta- level. We then discuss how the combination of explicit induction axioms and backward-reasoning enables automated loop splitting, which is the key for verifying advanced array-properties. We conclude the first part of the thesis by generalizing the trace-logic-based verification framework to support multiple execution traces and relational properties. In the second part of the thesis, we apply superposition-based theorem proving, and in particular the state-of-the-art theorem prover VAMPIRE, to reason about the validity statements of the trace logic domain. We introduce two techniques, layered clause selection and subsumption demodulation, which are crucial for efficient superposition-based reasoning in the trace logic domain. Moreover, to ease the manual analysis of both proofs and failed proof attempts, we describe a tool, which interactively visualizes proof attempts of saturation-based theorem provers. Finally, we provide an experimental evaluation of the trace-logic-based verification framework on interesting sets of benchmarks, which cover challenging properties of software programs including loops and arrays. The presented results suggest that our superposition-based verification framework is an interesting alternative to existing SMT-based verification approaches.
URI: https://doi.org/10.34726/hss.2020.86611
DOI: 10.34726/hss.2020.86611
Library ID: AC16102536
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Feb 21, 2021


checked on Feb 21, 2021

Google ScholarTM


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