TU Darmstadt / ULB / TUbiblio

Assessing the Coverage of Formal Specifications (Extended Abstract)

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 Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen