Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-41202-8_5
Title: A proof slicing framework for program verification
Authors: Le, T.C.
Gherghina, C.
Voicu, R. 
Chin, W.-N. 
Issue Date: 2013
Citation: Le, T.C.,Gherghina, C.,Voicu, R.,Chin, W.-N. (2013). A proof slicing framework for program verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8144 LNCS : 53-69. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-41202-8_5
Abstract: 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. © 2013 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/77977
ISBN: 9783642412011
ISSN: 03029743
DOI: 10.1007/978-3-642-41202-8_5
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

74
checked on Dec 29, 2019

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.