Formalizing a framework for dynamic slicing of program dependence graphs in Isabelle/HOL

被引：0

作者：

Wasserrab, Daniel ^{[1
]}

Lochbihler, Andreas ^{[1
]}

机构：

[1] Univ Karlsruhe, Karlsruhe, Germany

来源：

THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS | 2008年 / 5170卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Slicing is a widely-used technique with applications in e.g. compiler technology and software security. Thus verification of algorithms in these areas is often based on the correctness of slicing, which should ideally be proven independent of concrete programming languages and with the help of well-known verifying techniques such as proof assistants. As a first step in this direction, this contribution presents a framework for dynamic slicing based on control flow and program dependence graphs and machine checked in Isabelle/HOL. Abstracting from concrete syntax we base the framework on a graph representation of the program fulfilling certain structural and well-formedness properties.

引用

页码：294 / 309

页数：16

共 50 条

[21] An Isabelle/HOL Framework for Synthetic Completeness Proofs [J].

From, Asta Halkjaer .

PROCEEDINGS OF THE 14TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2025, 2025, :171-186

[22] Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL [J].

Echenim, Mnacho ;

Guiol, Hervé ;

Peltier, Nicolas .

Journal of Automated Reasoning, 2019, 64 (04) :737-765

[23] Formalizing Java']Java dynamic loading in HOL [J].

Zuo, TJ ;

Han, JG ;

Chen, P .

THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2004, 3223 :287-304

[24] Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem [J].

Kharim, Aabid Seeyal Abdul ;

Prathamesh, T. V. H. ;

Rajiv, Shweta ;

Vyas, Rishi .

INTELLIGENT COMPUTER MATHEMATICS, CICM 2023, 2023, 14101 :158-173

[25] An Extension of the Framework Types-To-Sets for Isabelle/HOL [J].

Milehins, Mihails .

PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, :180-196

[26] Formalizing executable dynamic and forward slicing [J].

Binkley, D ;

Danicic, S ;

Gyimóthy, T ;

Harman, M ;

Kiss, A ;

Ouarbya, L .

FOURTH IEEE INTERNATIONAL WORKSHOP ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2004, :43-52

[27] Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL [J].

Soualah, Sohaib ;

Khalgui, Mohamed ;

Chaoui, Allaoua .

ADVANCED INFORMATION NETWORKING AND APPLICATIONS, VOL 2, AINA 2024, 2024, 200 :199-212

[28] Model Checking with Program Slicing Based on Variable Dependence Graphs [J].

Matsubara, Masahiro ;

Sakurai, Kohei ;

Narisawa, Fumio ;

Enshoiwa, Masushi ;

Yamane, Yoshio ;

Yamanaka, Hisamitsu .

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (105) :56-68

[29] A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL [J].

Marmsoler, Diego .

FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018, 2018, 11232 :251-269

[30] Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL [J].

Armstrong, Alasdair ;

Struth, Georg ;

Weber, Tjark .

INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 :197-212

← 1 2 3 4 5 →