Enhancing Theorem Prover Interfaces with Program Slice Information

This paper proposes an extension to theorem proving interfaces for use with proofdirected debugging and other disproof-based applications. The extension is based around tracking a user-identified set of rules to create an informative program slice. Information is collected based on the involvement of these rules in both successful and unsuccessful proof branches. This provides a heuristic score for making judgements about the correctness of any rule. A simple mechanism for syntax highlighting based on such information is proposed and a small case study presented illustrating its operation. No implementation of these ideas yet exists. Key words: Proof-Directed Debugging, Program Slicing, Verification

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Louise A. Dennis
• Keywords: ENTCS 2007, Informative Program Slice, Small Case Study, Unsuccessful Proof Branches