Abstract
Backward slicers are typically path-insensitive (i.e., they ignore the evaluation of predicates at conditional branches) often producing too big slices. Though the effect of path-sensitivity is always desirable, the major challenge is that there are, in general, an exponential number of predicates to be considered. We present a path-sensitive backward slicer and demonstrate its practicality with real C programs. The crux of our method is a symbolic execution-based algorithm that excludes spurious dependencies lying on infeasible paths and avoids imprecise joins at merging points while reusing dependencies already computed by other paths, thus pruning the search space significantly.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: PLDI 2001, pp. 203–213 (2001)
Bent, L., Atkinson, D.C., Griswold, W.G.: A Comparative Study of Two Whole Program Slicers for C. Technical report, University of California at San Diego, La Jolla (2001)
Canfora, G., Cimitile, A., De Lucia, A.: Conditioned Program Slicing. Information and Software Technology 40(11-12), 595–607 (1998)
Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008)
Craig, W.: Three Uses of Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. Journal of Symbolic Computation 22 (1955)
Daoudi, M., Ouarbya, L., Howroyd, J., Danicic, S., Harman, M., Fox, C., Ward, M.P.: Consus: A Scalable Approach to Conditioned Slicing. In: WCRE 2002, pp. 109–118 (2002)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice-Hall (1976)
Field, J., Ramalingam, G., Tip, F.: Parametric Program Slicing. In: POPL 1995, pp. 379–392 (1995)
Fischer, J., Jhala, R., Majumdar, R.: Joining Dataflow with Predicates. In: ESEC/FSE-13, pp. 227–236 (2005)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from Proofs. In: POPL 2004, pp. 232–244 (2004)
Horwitz, S., Reps, T., Binkley, D.: Interprocedural Slicing using Dependence Graphs. In: PLDI 1988, pp. 35–46 (1988)
Jaffar, J., Navas, J.A., Santosa, A.E.: Unbounded Symbolic Execution for Program Verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 396–411. Springer, Heidelberg (2012)
Jaffar, J., Santosa, A.E., Voicu, R.: Efficient Memoization for Dynamic Programming with Ad-hoc Constraints. In: AAAI 2008, pp. 297–303 (2008)
Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: A Symbolic Execution Tool for Verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758–766. Springer, Heidelberg (2012)
Lalire, G., Argoud, M., Jeannet, B.: The Interproc Analyzer (2009), http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc
McMillan, K.L.: Lazy Annotation for Program Testing and Verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104–118. Springer, Heidelberg (2010)
Seo, S., Yang, H., Yi, K.: Automatic Construction of Hoare Proofs from Abstract Interpretation Results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 230–245. Springer, Heidelberg (2003)
Snelting, G., Robschink, T., Krinke, J.: Efficient Path Conditions in Dependence Graphs for Software Safety Analysis. In: TOSEM 2006, vol. 15, pp. 410–457 (2006)
Weiser, M.: Program Slicing. In: ICSE 1981, pp. 439–449 (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E. (2012). Path-Sensitive Backward Slicing. In: Miné, A., Schmidt, D. (eds) Static Analysis. SAS 2012. Lecture Notes in Computer Science, vol 7460. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33125-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-33125-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33124-4
Online ISBN: 978-3-642-33125-1
eBook Packages: Computer ScienceComputer Science (R0)