Skip to Main content Skip to Navigation
Conference papers

Verified Validation of Program Slicing

Sandrine Blazy 1 Andre Maroneze 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Program slicing is a well-known program transformation which simplifies a program with respect to 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 de-pendence 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 interme-diate language of the compiler having the same expressiveness as C. Our experiments show that our formally verified validator scales on large realistic programs.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-01110821
Contributor : David Pichardie <>
Submitted on : Wednesday, January 28, 2015 - 11:52:06 PM
Last modification on : Thursday, January 7, 2021 - 4:30:04 PM

Links full text

Identifiers

Citation

Sandrine Blazy, Andre Maroneze, David Pichardie. Verified Validation of Program Slicing. CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, ⟨10.1145/2676724.2693169⟩. ⟨hal-01110821⟩

Share

Metrics

Record views

1272