Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Downloads (Pure)

Abstract

Deductive verification can be used to ensure properties about all possible behaviours of a program, even when the program is parameterised and has an unbounded state space. But to achieve this, the user needs to specify what the desired properties are, and often needs to guide the prover with auxiliary annotations. This paper investigates what annotations are actually needed, and it provides a taxonomy to categorise these annotations. In particular, we identify several top-level categories, which are further divided into subcategories of annotations. This taxonomy is then used as a basis to investigate how often particular annotation categories occur, by inspecting over 10k lines of annotated programs. To determine whether the results are in line with expectations, we have interviewed several experts on deductive verification. Moreover, we show how the results can be used to evaluate the effectiveness of annotation generators. The knowledge from this analysis provides a gateway to guide further research in improving the efficiency of deductive verification, e.g.: it can serve as a guideline on what categories of annotations should be generated automatically, to evaluate the power of existing annotation generation techniques, and to improve the teaching of deductive verification.
Original languageEnglish
Title of host publicationProceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022
PublisherIEEE/EUCA
Pages69-79
Number of pages11
ISBN (Electronic)9781450392877
ISBN (Print)978-1-6654-5208-3
DOIs
Publication statusPublished - 20 Jun 2022
EventIEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022 - Pittsburgh, United States
Duration: 22 May 202223 May 2022
Conference number: 10

Conference

ConferenceIEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022
Abbreviated titleFormaliSE 2022
Country/TerritoryUnited States
CityPittsburgh
Period22/05/2223/05/22

Keywords

  • Annotations
  • Taxonomy
  • Deductive verification
  • Software verification
  • Specification languages

Fingerprint

Dive into the research topics of 'Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers'. Together they form a unique fingerprint.

Cite this