research-article

Verified Validation of Program Slicing

Authors:

Sandrine Blazy,

Andre Maroneze,

David PichardieAuthors Info & Claims

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

Pages 109 - 117

https://doi.org/10.1145/2676724.2693169

Published: 13 January 2015 Publication History

Abstract

Program slicing is a well-known program transformation which simplifies a program wrt a given criterion while preserving its semantics. Since the seminal paper published by Weiser in 1981, program slicing is still widely used in various application domains. State of the art program slicers operate over program dependence graphs (PDG), a sophisticated data structure combining data and control dependences.

In this paper, we follow the a posteriori validation approach to formally verify (in Coq) a general program slicer. Our validator for program slicing is efficient and validates the results of a run of an unverified program slicer. Program slicing is interesting for a posteriori validation because the correctness proof of program slicing requires to compute new supplementary information from the PDG, thus decoupling the slicing algorithm from its proof.

Our semantics-preserving program slicer is integrated into the CompCert formally verified compiler. It operates over an intermediate language of the compiler having the same expressiveness as C. Our experiments show that our formally verified validator scales on large realistic programs.

References

[1]

Companion website. http://www.irisa.fr/celtique/ext/slicing.

[2]

T. Amtoft. Slicing for modern program structures: a theory for eliminating irrelevant loops. Information Processing Letters, 106(2):45--51, 2008.

Digital Library

[3]

J. B. Barros, D. da Cruz, P. R. Henriques, and J. S. Pinto. Assertion- based slicing and slice graphs. Formal Aspects of Computing, 24(2):217--248, 2012.

[4]

G. Barthe, D. Demange, and D. Pichardie. A formally verified SSA-based middle-end - static single assignment meets CompCert. In European Symposium on Programming (ESOP), volume 7211 of LNCS, pages 47--66. Springer, 2012.

Digital Library

[5]

Y. Bertot, B. Grégoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Proc. of TYPES 2006, volume 3839 of LNCS, pages 66--81. Springer, 2006.

Digital Library

[6]

S. Blazy, V. Laporte, A. Maroneze, and D. Pichardie. Formal verification of a C value analysis based on abstract interpretation. In Static Analysis Symposium (SAS), pages 324--344, 2013.

[7]

S. Blazy, A. Maroneze, and D. Pichardie. Formal verification of loop bound estimation for WCET analysis. In Verified Software: Theories, Tools, Experiments (VSTTE 2013), LNCS, pages 281--303. Springer, 2013.

[8]

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu. Extracting a data flow analyser in constructive logic. Theoretical Computer Science, 342(1):56--78, 2005.

Digital Library

[9]

T. CompCert development team. The CompCert formally verified compiler, version 2.4, 2008--2014. http://compcert.inria.fr.

[10]

S. Conchon, J. Filliâtre, and J. Signoles. Designing a generic graph library using ML functors. In Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, pages 124--140, 2007.

[11]

K. D. Cooper, T. J. Harvey, and K. Kennedy. A simple, fast dominance algorithm. Technical report, Rice university, 2000.

[12]

S. Coupet-Grimal and W. Delobel. A uniform and certified approach for two static analyses. In Proc. of TYPES 2004, volume 3839 of LNCS, pages 115--137, 2004.

Digital Library

[13]

J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst., 9(3):319--349, 1987.

Digital Library

[14]

J.-H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie. Formal verification of a C static analyzer. In 42nd symposium Principles of Programming Languages (POPL), 2015. To appear.

Digital Library

[15]

G. Klein and T. Nipkow. A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst., 28(4):619--695, 2006.

Digital Library

[16]

T. Lengauer and R. E. Tarjan. A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst., 1(1):121--141, 1979.

Digital Library

[17]

X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107--115, 2009.

Digital Library

[18]

S. S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997.

Digital Library

[19]

G. Necula. Translation validation for an optimizing compiler. SIGPLAN Not., 35(5):83--94, 2000.

Digital Library

[20]

F. Nielson, H. R. Nielson, and C. Hankin. Principles of program analysis. Springer, 1999.

Digital Library

[21]

T. Nipkow. Abstract interpretation of annotated commands. In Interactive Theorem Proving (ITP), volume 7406 of LNCS, pages 116--132. Springer, 2012.

[22]

C. Okasaki and A. Gill. Fast mergeable integer maps. In Workshop on ML, pages 77--86, 1998.

[23]

V. P. Ranganath, T. Amtoft, A. Banerjee, J. Hatcliff, and M. B. Dwyer. A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst., 29(5), 2007.

Digital Library

[24]

T. Reps and W. Yang. The semantics of program slicing and program integration. In TAPSOFT'89, pages 360--374. Springer, 1989.

Digital Library

[25]

F. Tip. A survey of program slicing techniques. J. Prog. Lang., 3(3), 1995.

[26]

J.-B. Tristan and X. Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In 35th symposium Principles of Programming Languages (POPL), pages 17--27. ACM Press, 2008.

Digital Library

[27]

D. Wasserrab. From Formal Semantics to Verified Slicing - A Modular Framework with Applications in Language Based Security. PhD thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, Oct. 2010.

[28]

D. Wasserrab and A. Lochbihler. Formalizing a framework for dynamic slicing of program dependence graphs in Isabelle/HOL. In TPHOLs, volume 5170 of LNCS, pages 294--309. Springer, 2008.

Digital Library

[29]

M. Weiser. Program slicing. In S. Jeffrey and L. G. Stucki, editors, Int. Conf. on Software Engineering (ICSE), pages 439--449. IEEE Computer Society, 1981.

Digital Library

[30]

B. Xu, J. Qian, X. Zhang, Z. Wu, and L. Chen. A brief survey of program slicing. SIGSOFT Softw. Eng. Notes, 30(2):1--36, Mar. 2005.

Digital Library

[31]

J. Zhao, S. Nagarakatte, M. Martin, and S. Zdancewic. Formal verification of SSA-based optimizations for LLVM. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, pages 175--186, New York, NY, USA, 2013. ACM.

Digital Library

[32]

J. Zhao and S. Zdancewic. Mechanized verification of computing dominators for formalizing compilers. In Certified Programs and Proofs - Second International Conference, CPP 2012, pages 27--42. Springer, 2012.

Digital Library

[33]

J. Zhao, S. Zdancewic, S. Nagarakatte, and M. Martin. Formalizing the LLVM intermediate representation for verified program transformation. In 39th symposium Principles of Programming Languages (POPL'12), pages 427--440. ACM, 2012.

Digital Library

Cited By

Léchenet JKosmatov NLe Gall P(2023)Efficient Computation of Arbitrary Control DependenciesTheoretical Computer Science10.1016/j.tcs.2023.114029(114029)Online publication date: Jun-2023
https://doi.org/10.1016/j.tcs.2023.114029
Blatter LKosmatov NPrevosto VLe Gall P(2022)An Efficient VCGen-Based Modular Verification of Relational PropertiesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_28(498-516)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19849-6_28
Blatter LKosmatov NPrevosto VLe Gall P(2022)Certified Verification of Relational PropertiesIntegrated Formal Methods10.1007/978-3-031-07727-2_6(86-105)Online publication date: 1-Jun-2022
https://doi.org/10.1007/978-3-031-07727-2_6
Show More Cited By

Index Terms

Verified Validation of Program Slicing
1. General and reference
  1. Cross-computing tools and techniques
    1. Validation
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Empirical software validation
      2. Process validation

Recommendations

Abstract Program Slicing: An Abstract Interpretation-Based Approach to Program Slicing

In the present article, we formally define the notion of abstract program slicing, a general form of program slicing where properties of data are considered instead of their exact value. This approach is applied to a language with numeric and reference ...
A brief survey of program slicing

Program slicing is a technique to extract program parts with respect to some special computation. Since Weiser first proposed the notion of slicing in 1979, hundreds of papers have been presented in this area. Tens of variants of slicing have been ...
Using Relational Verification for Program Slicing
Software Engineering and Formal Methods
Abstract
Program slicing is the process of removing statements from a program such that defined aspects of its behavior are retained. For producing precise slices, i.e., slices that are minimal in size, the program’s semantics must be considered. Existing ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

January 2015

192 pages

ISBN:9781450332965

DOI:10.1145/2676724

Program Chairs:
Xavier Leroy
Inria Paris-Rocquencourt, France
,
Alwen Tiu
Nanyang Technological University, Singapore

Copyright © 2015 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 the author(s) 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

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Agence Nationale de la Recherche

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 13 - 14, 2015

Mumbai, India

Acceptance Rates

CPP '15 Paper Acceptance Rate 18 of 26 submissions, 69%;

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
181
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Léchenet JKosmatov NLe Gall P(2023)Efficient Computation of Arbitrary Control DependenciesTheoretical Computer Science10.1016/j.tcs.2023.114029(114029)Online publication date: Jun-2023
https://doi.org/10.1016/j.tcs.2023.114029
Blatter LKosmatov NPrevosto VLe Gall P(2022)An Efficient VCGen-Based Modular Verification of Relational PropertiesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_28(498-516)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19849-6_28
Blatter LKosmatov NPrevosto VLe Gall P(2022)Certified Verification of Relational PropertiesIntegrated Formal Methods10.1007/978-3-031-07727-2_6(86-105)Online publication date: 1-Jun-2022
https://doi.org/10.1007/978-3-031-07727-2_6
Amtoft TBanerjee A(2020)A Theory of Slicing for Imperative Probabilistic ProgramsACM Transactions on Programming Languages and Systems10.1145/337289542:2(1-71)Online publication date: 17-Apr-2020
https://dl.acm.org/doi/10.1145/3372895
Amtoft TAndroutsopoulos KClark D(2020)Correctly Slicing Extended Finite State MachinesFrom Lambda Calculus to Cybersecurity Through Program Analysis10.1007/978-3-030-41103-9_6(149-197)Online publication date: 15-Feb-2020
https://doi.org/10.1007/978-3-030-41103-9_6
Stolarek JCheney J(2019)Verified Self-Explaining ComputationMathematics of Program Construction10.1007/978-3-030-33636-3_4(76-102)Online publication date: 20-Oct-2019
https://doi.org/10.1007/978-3-030-33636-3_4
Heinze TTurker J(2018)Certified Information Flow Analysis of Service Implementations2018 IEEE 11th Conference on Service-Oriented Computing and Applications (SOCA)10.1109/SOCA.2018.00033(177-184)Online publication date: Nov-2018
https://doi.org/10.1109/SOCA.2018.00033
Léchenet JKosmatov NLe Gall P(2018)Fast Computation of Arbitrary Control DependenciesFundamental Approaches to Software Engineering10.1007/978-3-319-89363-1_12(207-224)Online publication date: 4-Apr-2018
https://doi.org/10.1007/978-3-319-89363-1_12
Léchenet JKosmatov NLe Gall P(2017)Cut branches before looking for bugs: certifiably sound verification on relaxed slicesFormal Aspects of Computing10.1007/s00165-017-0439-x30:1(107-131)Online publication date: 9-Oct-2017
https://doi.org/10.1007/s00165-017-0439-x
Léchenet JKosmatov NGall P(2016)Cut Branches Before Looking for BugsProceedings of the 19th International Conference on Fundamental Approaches to Software Engineering - Volume 963310.1007/978-3-662-49665-7_11(179-196)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49665-7_11
Show More Cited By

View Options

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.

Figures

Tables

Media

View Table of Conten