Description
Logical proofs are playing an increasingly important role in the design of reliable software systems. In several applications, it is necessary to store, manipulate and transfer explicit representations of such proofs. It is desirable that the proofs be represented in a compact format, without incurring any loss of information and without performance penalties with respect to access and manipulation. This thesis describes methods for proof optimization in the context of Proof-Carrying Code (PCC).
Most of the proofs we encounter in program verification are proofs in first-order logic. Furthermore, in many cases predicates contain portions whose proof is uniquely determined by the logic. A proof checker can be made to internally reconstruct the proof in such cases, thus freeing the proof producer from encoding explicit proofs for them. This simple optimization, which we call inversion optimization reduces the size of proofs by 37%. We also describe an orthogonal optimization, which we call lemma extraction, that attempts to replace repeated occurrences of similar subproofs by instances of a more general lemma. We propose a few variants based on this general idea with varying degrees of applicability. By using this optimization, we obtain a further reduction of 15% in the size of the proofs.