TY - GEN
T1 - Modular indirect push-button formal verification of multi-threaded code generators
AU - Wijs, Anton
AU - Wiłkowski, Maciej
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85072870350&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-30446-1_22
DO - 10.1007/978-3-030-30446-1_22
M3 - Conference contribution
AN - SCOPUS:85072870350
SN - 978-3-030-30445-4
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 410
EP - 429
BT - Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Proceedings
A2 - Ölveczky, Peter Csaba
A2 - Salaün, Gwen
PB - Springer
CY - Cham
T2 - 17th International Conference on Software Engineering and Formal Methods, SEFM 2019
Y2 - 18 September 2019 through 20 September 2019
ER -