Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL

DOI10.1007/978-3-540-71067-7_24zbMath1165.68477OpenAlexW1578467191MaRDI QIDQ3543667

Daniel Wasserrab, Andreas Lochbihler

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://publikationen.bibliothek.kit.edu/1000008488/706398

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• Slicing

Cites Work

• Unnamed Item
• Unnamed Item
• Slicing for modern program structures: a theory for eliminating irrelevant loops
• Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures
• Dynamic slicing: a generic analysis based on a natural semantics format
• Formal certification of a compiler back-end or
• Types for Proofs and Programs

This page was built for publication: Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL