TY  - JOUR
A1  - Bandyopadhyay, Soumyadip
A1  - Sarkar, Dipankar
A1  - Mandal, Chittaranjan
A1  - Giese, Holger
T1  - Translation validation of coloured Petri net models of programs on integers
T2  - Acta informatica
N2  - Programs are often subjected to significant optimizing and parallelizing transformations based on extensive dependence analysis. Formal validation of such transformations needs modelling paradigms which can capture both control and data dependences in the program vividly. Being value-based with an inherent scope of capturing parallelism, the untimed coloured Petri net (CPN) models, reported in the literature, fit the bill well; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential variable-based IRs like sequential control flow graphs (CFGs). In this work, an efficient path-based equivalence checking method for CPN models of programs on integers is presented. Extensive experimentation has been carried out on several sequential and parallel examples. Complexity and correctness issues have been treated rigorously for the method.
Y1  - 2022
UR  - https://publishup.uni-potsdam.de/frontdoor/index/index/docId/63643
SN  - 0001-5903
SN  - 1432-0525
VL  - 59
IS  - 6
SP  - 725
EP  - 759
PB  - Springer
CY  - New York
ER  -