Abstract
We present a general approach on how to integrate a semi-automatic verification tool into a state-of-the-art integrated development environment (IDE). The objective and challenge is to keep implementation, specification and proofs in sync. Following a change in one of the specifications or implementations, all proofs that could possibly be affected by that change are rescheduled. To improve performance we look at several optimizations. User feedback about proof results is provided within the IDE using standard markers and views. The approach has been implemented and realizes an integration of the interactive verification system KeY into the Eclipse IDE. © 2014 Springer International Publishing.
Author supplied keywords
Cite
CITATION STYLE
Hentschel, M., Käsdorf, S., Hähnle, R., & Bubel, R. (2014). An interactive verification tool meets an IDE. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8739 LNCS, pp. 55–70). Springer Verlag. https://doi.org/10.1007/978-3-319-10181-1_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
