Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification

TL;DR

This paper introduces a generic method for generating proof objects for symbolic execution parameters, demonstrated through antiunification, with an implementation and evaluation on C and Java inputs.

Contribution

It presents a novel approach for proof object generation in symbolic execution, specifically for antiunification, with an implementation and empirical evaluation.

Findings

Proof objects can be generated and checked for antiunification.

The method is applicable to real-world programming languages.

Proof object sizes are analyzed for C and Java inputs.

Abstract

Symbolic execution uses various algorithms (matching, (anti)unification), whose executions are parameters for proof object generation. This paper proposes a generic method for generating proof objects for such parameters. We present in detail how our method works for the case of antiunification. The approach is accompanied by an implementation prototype, including a proof object generator and a proof object checker. In order to investigate the size of the proof objects, we generate and check proof objects for inputs inspired from the K definitions of C and Java.