TU Darmstadt / ULB / TUbiblio

Assessing the Coverage of Formal Specifications (Extended Abstract)

Steinhöfel, Dominic
Ábrahám, Erika and Tarifa, Lizeth Tapia (eds.) (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), University of Oslo, pp. 38-40, [Online-Edition: https://www.duo.uio.no/bitstream/handle/10852/57814/uioRepor...],
[Book Section]

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.

Item Type: Book Section
Erschienen: 2017
Editors: Ábrahám, Erika and Tarifa, Lizeth Tapia
Creators: Steinhöfel, Dominic
Title: Assessing the Coverage of Formal Specifications (Extended Abstract)
Language: German
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.

Title of Book: Proceedings of the PhD Symposium at iFM’17 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’17)
Publisher: University of Oslo
ISBN: 978-82-7368-435-6
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Date Deposited: 11 Sep 2017 10:11
Official URL: https://www.duo.uio.no/bitstream/handle/10852/57814/uioRepor...
Identification Number: TUD-CS-2017-0242
Export:

Optionen (nur für Redakteure)

View Item View Item