2013 | OriginalPaper | Chapter
A Proof Slicing Framework for Program Verification
Authors : Ton Chanh Le, Cristian Gherghina, Razvan Voicu, Wei-Ngan Chin
Published in: Formal Methods and Software Engineering
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In the context of program verification, we propose a
formal framework
for
proof slicing
that can aggressively reduce the size of proof obligations as a means of performance improvement. In particular, each large proof obligation may be broken down into smaller proofs, for which the overall processing cost can be greatly reduced, and be even more effective under
proof caching
. Our proposal is built on top of existing automatic provers, including the state-of-the-art prover Z3, and can also be viewed as a re-engineering effort in proof decomposition that attempts to avoid large-sized proofs for which these provers may be particularly inefficient. In our approach, we first develop a calculus that formalizes a
complete proof slicing
procedure, which is followed by the development of an
aggressive proof slicing
method. Retaining completeness is important, and thus in our experiments the complete method serves as a backup for the cases when the aggressive procedure fails. The foundations of the aggressive slicing procedure are based on a novel lightweight annotation scheme that captures
weak links
between sub-formulas of a proof obligation; the annotations can be inferred automatically in practice, and thus both methods are fully automated.