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.
Type de document :
Communication dans un congrès
CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, 〈10.1145/2676724.2693169〉
Liste complète des métadonnées
Contributeur : David Pichardie <>
Soumis le : mercredi 28 janvier 2015 - 23:52:06
Dernière modification le : jeudi 15 novembre 2018 - 11:57:41

Lien texte intégral



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〉



Consultations de la notice