Towards Trace-based Deductive Verification (Tech Report)

TL;DR

This paper introduces a logic over symbolic traces for modular, trace-based deductive verification of recursive procedures, overcoming limitations of traditional contract-based methods by enabling specifications involving event sequences.

Contribution

It presents a novel logic and deduction system for trace-based verification, extending contract-based approaches to handle event sequences in recursive procedures.

Findings

Proposed a sound deduction system based on symbolic execution and induction.

Generalized contract-based verification to trace-based methods.

Enables specifying procedures with event sequences in a modular way.

Abstract

Contracts specifying a procedure's behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification.