Steinhöfel, Dominic
Hrsg.: Ábrahám, Erika ; Tarifa, Lizeth Tapia (2017)
Assessing the Coverage of Formal Specifications (Extended Abstract).
In: Proceedings of the PhD Symposium at iFM’17 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’17)
Buchkapitel, Bibliographie
Kurzbeschreibung (Abstract)
Deductive program verification is an intricate and time-consuming task, in spite of significant advances in state-of-the-art program provers. While proving the correctness of programs with respect to existing specifications can already be difficult, it can be even more demanding to come up with sensible specifications for methods and especially for loops. Another issue is related to programs heavily making use of software libraries: Their verification can be considered almost infeasible due to the lack of formal specifications of the libraries. We propose a method for assessing the coverage/strength of formal specifications based on “facts” extracted using heavyweight symbolic execution. We envision that this method can be employed for (1) assisting verification engineers in the incremental specification of programs, (2) comparing different specifications for the same program, and (3) obtaining information for specification generation tools. Our approach has been implemented as a prototype for Java which uses the heavyweight symbolic execution system KeY as a backend. We studied its practicability with several small examples and plan to conduct a more extensive case study in the near future.
| Typ des Eintrags: | Buchkapitel |
|---|---|
| Erschienen: | 2017 |
| Herausgeber: | Ábrahám, Erika ; Tarifa, Lizeth Tapia |
| Autor(en): | Steinhöfel, Dominic |
| Art des Eintrags: | Bibliographie |
| Titel: | Assessing the Coverage of Formal Specifications (Extended Abstract) |
| Sprache: | Deutsch |
| Publikationsjahr: | September 2017 |
| Verlag: | University of Oslo |
| Buchtitel: | Proceedings of the PhD Symposium at iFM’17 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’17) |
| URL / URN: | https://www.duo.uio.no/bitstream/handle/10852/57814/uioRepor... |
| Kurzbeschreibung (Abstract): | Deductive program verification is an intricate and time-consuming task, in spite of significant advances in state-of-the-art program provers. While proving the correctness of programs with respect to existing specifications can already be difficult, it can be even more demanding to come up with sensible specifications for methods and especially for loops. Another issue is related to programs heavily making use of software libraries: Their verification can be considered almost infeasible due to the lack of formal specifications of the libraries. We propose a method for assessing the coverage/strength of formal specifications based on “facts” extracted using heavyweight symbolic execution. We envision that this method can be employed for (1) assisting verification engineers in the incremental specification of programs, (2) comparing different specifications for the same program, and (3) obtaining information for specification generation tools. Our approach has been implemented as a prototype for Java which uses the heavyweight symbolic execution system KeY as a backend. We studied its practicability with several small examples and plan to conduct a more extensive case study in the near future. |
| ID-Nummer: | TUD-CS-2017-0242 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 11 Sep 2017 10:11 |
| Letzte Änderung: | 22 Nov 2018 08:32 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum