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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Amir, E., McIlraith, S.: Partition-based logical reasoning for first-order and propositional theories. Artificial Intelligence 162, 49–88 (2005)
Biere, A., Sinz, C.: Decomposing SAT problems into connected components. JSAT (2006)
Buss, S.R.: An introduction to proof theory. In: Handbook of Proof Theory (1998)
de Moura, L., Bjørner, N.: Relevancy propagation. Technical report, MSR (2007)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Do, H., Elbaum, S.G., Rothermel, G.: Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. In: ESE, vol. 10 (2005)
Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. SIGSAM Bulletin 31, 2–9 (1997)
Fietzke, A., Weidenbach, C.: Labelled splitting. Annals of MAI 55 (2009)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)
Huang, H., Tsai, W.-T., Paul, R.A.: Proof slicing with application to model checking web services. In: ISORC, pp. 292–299 (2005)
Klarlund, N., Moller, A.: MONA Version 1.4 - User Manual. BRICS Notes Series (2001)
Lang, J., Liberatore, P., Marquis, P.: Propositional independence: formula-variable independence and forgetting. Journal of Artificial Intelligence Research 18 (2003)
Le, T.C., Gherghina, C., Voicu, R., Chin, W.N.: A Proof Slicing Framework for Program Verification (2013), http://www.comp.nus.edu.sg/~chanhle/icfem13-long.pdf
Leino, K.R.M., Moskal, M., Schulte, W.: Verification condition splitting (2008)
McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 41–57 (2009)
Navarro Pérez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI, pp. 556–566 (2011)
Nguyen, H.H., David, C., Qin, S.C., Chin, W.N.: Automated Verification of Shape And Size Properties via Separation Logic. In: VMCAI, pp. 251–266 (2007)
O’Hearn, P.W., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Park, T.J., Gelder, A.V.: Partitioning methods for satisfiability testing on large formulas. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 748–762. Springer, Heidelberg (1996)
Pugh, W.: The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM 8, 102–114 (1992)
Hong, H.S., Lee, I., Sokolsky, O.: Abstract slicing: A new approach to program slicing based on abstract interpretation and model checking. In: SCAM (2005)
Sørensen, U.: Slicing for Uppaal. Technical report, AALBORG University (2008)
Frama-C Software Analyser System (2012), http://frama-c.com
Torres-Jimenez, J., Vega-Garcia, L., Coutino-Gomez, C.A., Cartujano-Escobar, F.J.: SSTP: An approach to Solve SAT instances Through Partition. In: WSEAS (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Le, T.C., Gherghina, C., Voicu, R., Chin, WN. (2013). A Proof Slicing Framework for Program Verification. In: Groves, L., Sun, J. (eds) Formal Methods and Software Engineering. ICFEM 2013. Lecture Notes in Computer Science, vol 8144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41202-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-41202-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41201-1
Online ISBN: 978-3-642-41202-8
eBook Packages: Computer ScienceComputer Science (R0)