Proof Optimization Using Lemma Extraction

information presented here does not necessarily re ect the position or the policy of the Government and no oÆcial endorsement should be inferred. 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 trans-fer 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 verication are proofs in rst-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