Article

Path slicing

Authors:

Rupak MajumdarAuthors Info & Claims

PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation

Pages 38 - 47

https://doi.org/10.1145/1065010.1065016

Published: 12 June 2005 Publication History

Abstract

We present a new technique, path slicing, that takes as input a possibly infeasible path to a target location, and eliminates all the operations that are irrelevant towards the reachability of the target location. A path slice is a subsequence of the original path whose infeasibility guarantees the infeasibility of the original path, and whose feasibility guarantees the existence of some feasible variant of the given path that reaches the target location even though the given path may itself be infeasible. Our method combines the ability of program slicing to look at several program paths, with the precision that dynamic slicing enjoys by focusing on a single path. We have implemented Path Slicing to analyze possible counterexamples returned by the software model checker Blast. We show its effectiveness in drastically reducing the size of the counterexamples to less than 1% of their original size. This enables the precise verification of application programs (upto 100KLOC), by allowing the analysis to focus on the part of the counterexample that is relevant to the property being checked.

References

[1]

A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.

Digital Library

[2]

T. Ball, M. Naik, and S. K. Rajamani. From symptom to cause: Localizing errors in counterexample traces. In POPL 03: Principles of Programming Languages, pages 97--105. ACM, 2003.

Digital Library

[3]

T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL 02: Principles of Programming Languages, pages 1--3. ACM, 2002.

Digital Library

[4]

S. Basu, D. Saha, and S. A. Smolka. Localizing program errors for Cimple debugging. In FORTE 04: Formal Techniques for Networked and Distributed Systems, LNCS 3235, pages 79--96. Springer, 2004.

[5]

D. Beyer, A. Noack, and C. Lewerentz. Simple and efficient relational querying of software structures. In Proc. WCRE, pages 216--225. IEEE, 2003.

Digital Library

[6]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, 1986.

Digital Library

[7]

S. Chaki, J. Ouaknine, K. Yorav, and E. M. Clarke. Automated compositional abstraction refinement for concurrent C programs: A two-level approach. In SoftMC 03: Software Model Checking, 2003.

[8]

H. Chen and D. Wagner. MOPS: An infrastructure for examining security properties of software. In Proceedings of the 9th ACM Conference on Computer and Communications Security (CCS'02, Washington, DC), pages 235--244. ACM Press, 2002.

Digital Library

[9]

M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In PLDI 02: Programming Language Design and Implementation, pages 57--68. ACM, 2002.

Digital Library

[10]

E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

Digital Library

[11]

J. Field, G. Ramalingam, and F. Tip. Parametric program slicing. In POPL 95: Principles of Programming Languages, pages 379--392. ACM, 1995.

Digital Library

[12]

C. Flanagan, R. Joshi, X. Ou, and J. B. Saxe. Theorem proving using lazy proof explication. In CAV 03, LNCS, pages 355--367, 2003.

[13]

C. Flanagan and J. B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In POPL 00: Principles of Programming Languages, pages 193--205. ACM, 2000.

Digital Library

[14]

J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In PLDI 02: Programming Language Design and Implementation, pages 1--12. ACM, 2002.

Digital Library

[15]

Grammatech. Codesurfer 1.9. Technical report, 2004.

[16]

A. Groce and W. Visser. What went wrong: Explaining counterexamples. In SPIN 03: SPIN Workshop, LNCS 2648, pages 121--135. Springer, 2003.

Digital Library

[17]

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL 04: Principles of Programming Languages, pages 232--244. ACM, 2004.

Digital Library

[18]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL 02: Principles of Programming Languages, pages 58--70. ACM, 2002.

Digital Library

[19]

S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. ACM TOPLAS, 12:26--61, 1990.

Digital Library

[20]

B. Korel and J. Laski. Dynamic program slicing. Information Processing Letters, 29:155--163, 1988.

Digital Library

[21]

O. Lhotak and L. J. Hendren. Jedd: a BDD-based relational extension of Java. In PLDI 2004, pages 158--169, 2004.

Digital Library

[22]

M. Mock, D. C. Atkinson, C. Chambers, and S. J. Eggers. Improving program slicing with dynamic points-to data. In FSE 02: Foundations of Software Engineering, pages 71--80. ACM, 2002.

Digital Library

[23]

S. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24:217--298, 2002.

Digital Library

[24]

F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121--189, 1995.

[25]

M. Weiser. Program slices: formal, psychological, and practical investigations of an automatic program abstraction method. PhD thesis, 1979.

Digital Library

[26]

J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI 2004, pages 131--144. ACM, 2004.

Digital Library

[27]

X. Zhang and R. Gupta. Cost effective dynamic program slicing. In PLDI 04: Programming Language Design and Implementation, pages 94--106. ACM, 2004.

Digital Library

Cited By

Yadavally ALi YWang SNguyen T(2024)A Learning-Based Approach to Static Program SlicingProceedings of the ACM on Programming Languages10.1145/36498148:OOPSLA1(83-109)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649814
Beyer DKettl MLemberger T(2024)Fault Localization on Verification WitnessesModel Checking Software10.1007/978-3-031-66149-5_12(205-224)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_12
Han HKyea JJin YKang JPak BYun I(2023)QueryX: Symbolic Query on Decompiled Code for Finding Bugs in COTS Binaries2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179314(3279-3295)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179314
Show More Cited By

Index Terms

Path slicing

Recommendations

Path slicing
Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation

We present a new technique, path slicing, that takes as input a possibly infeasible path to a target location, and eliminates all the operations that are irrelevant towards the reachability of the target location. A path slice is a subsequence of the ...
Slicing Software for Model Construction

Applying finite-state verification techniques (e.g., model checking) to software requires that program source code be translated to a finite-state transition system that safely models program behavior. Automatically checking such a transition system for ...
Efficient Model Checking of Hardware Using Conditioned Slicing

In this work, we present an abstraction based property verification technique for hardware using conditioned slicing. We handle safety property specifications of the form G(antecedent@?consequent). We use the antecedent of the properties to create our ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation

June 2005

338 pages

ISBN:1595930566

DOI:10.1145/1065010

General Chair:
Vivek Sarkar
IBM Research
,
Program Chair:
Mary Hall
USC/ISI

ACM SIGPLAN Notices Volume 40, Issue 6
Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation
June 2005
325 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1064978
Issue’s Table of Contents

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 June 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI05

Sponsor:

PLDI05: ACM SIGPLAN Conference on Programming Language Design and Implementation 2005

June 12 - 15, 2005

IL, Chicago, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

105
Total Citations
View Citations
1,631
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)1

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yadavally ALi YWang SNguyen T(2024)A Learning-Based Approach to Static Program SlicingProceedings of the ACM on Programming Languages10.1145/36498148:OOPSLA1(83-109)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649814
Beyer DKettl MLemberger T(2024)Fault Localization on Verification WitnessesModel Checking Software10.1007/978-3-031-66149-5_12(205-224)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_12
Han HKyea JJin YKang JPak BYun I(2023)QueryX: Symbolic Query on Decompiled Code for Finding Bugs in COTS Binaries2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179314(3279-3295)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179314
Huang SWang X(2023)PExReport: Automatic Creation of Pruned Executable Cross-Project Failure Reports2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)10.1109/ICSE48619.2023.00027(184-195)Online publication date: May-2023
https://doi.org/10.1109/ICSE48619.2023.00027
Qasem AShirani PDebbabi MWang LLebel BAgba B(2021)Automatic Vulnerability Detection in Embedded Devices and FirmwareACM Computing Surveys10.1145/343289354:2(1-42)Online publication date: 5-Mar-2021
https://dl.acm.org/doi/10.1145/3432893
Mukelabai MBerger TBorba PJuristo N(2021)Semi-automated test-case propagation in fork ecosystemsProceedings of the 43rd International Conference on Software Engineering: New Ideas and Emerging Results10.1109/ICSE-NIER52604.2021.00018(46-50)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1109/ICSE-NIER52604.2021.00018
Sato RIwayama NKobayashi NHermenegildo MIgarashi A(2019)Combining higher-order model checking with refinement type inferenceProceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3294032.3294081(47-53)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3294032.3294081
Heo KLee WPashakhanloo PNaik MLie DMannan MBackes MWang X(2018)Effective Program Debloating via Reinforcement LearningProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243838(380-394)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243838
Beyer DLemberger THuchard MKästner CFraser G(2018)CPA-SymExec: efficient symbolic execution in CPAcheckerProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3240478(900-903)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3240478
Liu JWu DXue JHuchard MKästner CFraser G(2018)TDroid: exposing app switching attacks in Android with control flow specializationProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238188(236-247)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238188
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents