ABSTRACT
This paper proposes a framework, ProofStateViz, to visualize proof states and tactic transformations in interactive program verification, aiming to reduce cognitive load and improve proof comprehension for users of proof assistants.
PAPER · PDF
Loading PDF…
Key findings
ProofStateViz introduces a hierarchical proof state representation and tactic transformation graph.
The framework includes an interactive visualization interface integrated with IDE environments.
The approach aims to accelerate the learning curve for both novice and expert users.
Limitations & open questions
The effectiveness of the visualization approach needs empirical validation.
The scalability of the framework to more complex proof assistants is an open question.