Hentschel, Martin ; Käsdorf, Stefan ; Hähnle, Reiner ; Bubel, Richard
eds.: Albert, Elvira ; Sekerinski, Emil ; Zavattaro, Gianluigi (2014)
An interactive verification tool meets an IDE.
Conference or Workshop Item, Bibliographie
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.
| Item Type: | Conference or Workshop Item |
|---|---|
| Erschienen: | 2014 |
| Editors: | Albert, Elvira ; Sekerinski, Emil ; Zavattaro, Gianluigi |
| Creators: | Hentschel, Martin ; Käsdorf, Stefan ; Hähnle, Reiner ; Bubel, Richard |
| Type of entry: | Bibliographie |
| Title: | An interactive verification tool meets an IDE |
| Language: | German |
| Date: | September 2014 |
| Publisher: | Springer |
| Book Title: | Proceedings of the 11th International Conference on Integrated Formal Methods |
| Series: | LNCS |
| 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. |
| Identification Number: | TUD-CS-2014-0838 |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 31 Dec 2016 10:40 |
| Last Modified: | 03 Jun 2018 21:30 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum