Hello,I am a student in the 6th semster on TU Darmstadt and writing on my bachelor thesis about proof management for KeY <http://www.key-project.org/>. My mentor implemented the tool Visual DbC. It visualize Java code with JML contracts in a diagram based on the UML standard.
I added associations for all dependencies of prooves, identify changes in the Java code and JML contracts and compute wether a proof is deprecated or still valid.
I have a few Qestions for my related work section: How do you do the management of proofs in Isabelle? Are there any tools?Are there technics to react on changes of potential dependencies of proof? Could you detect wether a proof is still valid or deprecated? Are there tools for the dependencies of proofs? How are the dependencies visualized? I saw something like a dependency graph in JEdit. Is that correct?
Have you tools to refractor proofs or requirements?Thank you for taking the time to answer my questions. I look forward to your response.
Description: S/MIME Kryptografische Unterschrift