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.
Proof Optimization Using Lemma Extraction
Full Collection Name
Electrical Engineering & Computer Sciences Technical Reports
The Engineering Library
Researchers may make free and open use of the UC Berkeley Library’s digitized public domain materials. However, some materials in our online collections may be protected by U.S. copyright law (Title 17, U.S.C.). Use or reproduction of materials protected by copyright beyond that allowed by fair use (Title 17, U.S.C. § 107) requires permission from the copyright owners. The use or reproduction of some materials may also be restricted by terms of University of California gift or purchase agreements, privacy and publicity rights, or trademark law. Responsibility for determining rights status and permissibility of any use or reproduction rests exclusively with the researcher. To learn more or make inquiries, please see our permissions policies (https://www.lib.berkeley.edu/about/permissions-policies).