ITU

Effective Analysis of C Programs by Rewriting Variability

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Standard

Effective Analysis of C Programs by Rewriting Variability. / Iosif-Lazar, Alexandru Florin; Melo, Jean; Dimovski, Aleksandar; Brabrand, Claus; Wasowski, Andrzej.

In: The Art, Science, and Engineering of Programming, Vol. 1, No. 1, 1, 27.01.2017, p. 1-25.

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{8b16b6f1b72642709384db65d8d417b0,
title = "Effective Analysis of C Programs by Rewriting Variability",
abstract = "Context. Variability-intensive programs (program families) appear in many application areas and for many reasons today. Different family members, called variants, are derived by switching statically configurable options (features) on and off, while reuse of the common code is maximized.Inquiry. Verification of program families is challenging since the number of variants is exponential in the number of features. Existing single-program analysis and verification tools cannot be applied directly to program families, and designing and implementing the corresponding variability-aware versions is tedious and laborious.Approach. In this work, we propose a range of variability-related transformations for translating program families into single programs by replacing compile-time variability with run-time variability (non-determinism). The obtained transformed programs can be subsequently analyzed using the conventional off- the-shelf single-program analysis tools such as type checkers, symbolic executors, model checkers, and static analyzers.Knowledge. Our variability-related transformations are outcome-preserving, which means that the relation between the outcomes in the transformed single program and the union of outcomes of all variants derived from the original program family is equality.Grounding. We show our transformation rules and their correctness with respect to a minimal core imperative language IMP. Then, we discuss our experience of implementing and using the transformations for efficient and effective analysis and verification of real-world C program families.Importance. We report some interesting variability-related bugs that we discovered using various state-of-the-art single-program C verification tools, such as Frama-C, Clang, LLBMC.",
keywords = "ProgramFamilies, Variability-related Transformations, StaticAnalysis, Verification",
author = "Iosif-Lazar, {Alexandru Florin} and Jean Melo and Aleksandar Dimovski and Claus Brabrand and Andrzej Wasowski",
year = "2017",
month = jan,
day = "27",
doi = "10.22152/programming-journal.org/2017/1/1",
language = "English",
volume = "1",
pages = "1--25",
journal = "The Art, Science, and Engineering of Programming",
issn = "2473-7321",
number = "1",
note = "The Art, Science, and Engineering of Programming : ‹Programming› 2017, ‹Programming› 2017 ; Conference date: 03-04-2017 Through 06-04-2017",
url = "http://2017.programmingconference.org/",

}

RIS

TY - JOUR

T1 - Effective Analysis of C Programs by Rewriting Variability

AU - Iosif-Lazar, Alexandru Florin

AU - Melo, Jean

AU - Dimovski, Aleksandar

AU - Brabrand, Claus

AU - Wasowski, Andrzej

PY - 2017/1/27

Y1 - 2017/1/27

N2 - Context. Variability-intensive programs (program families) appear in many application areas and for many reasons today. Different family members, called variants, are derived by switching statically configurable options (features) on and off, while reuse of the common code is maximized.Inquiry. Verification of program families is challenging since the number of variants is exponential in the number of features. Existing single-program analysis and verification tools cannot be applied directly to program families, and designing and implementing the corresponding variability-aware versions is tedious and laborious.Approach. In this work, we propose a range of variability-related transformations for translating program families into single programs by replacing compile-time variability with run-time variability (non-determinism). The obtained transformed programs can be subsequently analyzed using the conventional off- the-shelf single-program analysis tools such as type checkers, symbolic executors, model checkers, and static analyzers.Knowledge. Our variability-related transformations are outcome-preserving, which means that the relation between the outcomes in the transformed single program and the union of outcomes of all variants derived from the original program family is equality.Grounding. We show our transformation rules and their correctness with respect to a minimal core imperative language IMP. Then, we discuss our experience of implementing and using the transformations for efficient and effective analysis and verification of real-world C program families.Importance. We report some interesting variability-related bugs that we discovered using various state-of-the-art single-program C verification tools, such as Frama-C, Clang, LLBMC.

AB - Context. Variability-intensive programs (program families) appear in many application areas and for many reasons today. Different family members, called variants, are derived by switching statically configurable options (features) on and off, while reuse of the common code is maximized.Inquiry. Verification of program families is challenging since the number of variants is exponential in the number of features. Existing single-program analysis and verification tools cannot be applied directly to program families, and designing and implementing the corresponding variability-aware versions is tedious and laborious.Approach. In this work, we propose a range of variability-related transformations for translating program families into single programs by replacing compile-time variability with run-time variability (non-determinism). The obtained transformed programs can be subsequently analyzed using the conventional off- the-shelf single-program analysis tools such as type checkers, symbolic executors, model checkers, and static analyzers.Knowledge. Our variability-related transformations are outcome-preserving, which means that the relation between the outcomes in the transformed single program and the union of outcomes of all variants derived from the original program family is equality.Grounding. We show our transformation rules and their correctness with respect to a minimal core imperative language IMP. Then, we discuss our experience of implementing and using the transformations for efficient and effective analysis and verification of real-world C program families.Importance. We report some interesting variability-related bugs that we discovered using various state-of-the-art single-program C verification tools, such as Frama-C, Clang, LLBMC.

KW - ProgramFamilies

KW - Variability-related Transformations

KW - StaticAnalysis

KW - Verification

U2 - 10.22152/programming-journal.org/2017/1/1

DO - 10.22152/programming-journal.org/2017/1/1

M3 - Journal article

VL - 1

SP - 1

EP - 25

JO - The Art, Science, and Engineering of Programming

JF - The Art, Science, and Engineering of Programming

SN - 2473-7321

IS - 1

M1 - 1

T2 - The Art, Science, and Engineering of Programming

Y2 - 3 April 2017 through 6 April 2017

ER -

ID: 81892925