Modular indirect push-button formal verification of multi-threaded code generators

Anton Wijs, Maciej Wiłkowski

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

2 Citations (Scopus)
2 Downloads (Pure)

Abstract

In model-driven development, the automated generation of a multi-threaded program based on a model specifying the intended system behaviour is an important step. Verifying that such a generation step semantically preserves the specified functionality is hard. In related work, code generators have been formally verified using theorem provers, but this is very time-consuming work, should be done by an expert in formal verification, and is not easily adaptable to changes applied in the generator. In this paper, we propose, as an alternative, a push-button approach, combining equivalence checking and code verification with previous results we obtained on the verification of generic code constructs. To illustrate the approach, we consider our Slco framework, which contains a multi-threaded Java code generator. Although the technique can still only be applied to verify individual applications of the generator, its push-button nature and efficiency in practice makes it very suitable for non-experts.

Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods - 17th International Conference, SEFM 2019, Proceedings
EditorsPeter Csaba Ölveczky, Gwen Salaün
Place of PublicationCham
PublisherSpringer
Pages410-429
Number of pages20
ISBN (Electronic)978-3-030-30446-1
ISBN (Print)978-3-030-30445-4
DOIs
Publication statusPublished - 2019
Event17th International Conference on Software Engineering and Formal Methods, SEFM 2019 - Oslo, Norway
Duration: 18 Sep 201920 Sep 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11724 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Conference on Software Engineering and Formal Methods, SEFM 2019
CountryNorway
CityOslo
Period18/09/1920/09/19

Fingerprint Dive into the research topics of 'Modular indirect push-button formal verification of multi-threaded code generators'. Together they form a unique fingerprint.

Cite this