[isabelle] Proofmanagement



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.

Jan Keller

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.