{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:32Z","timestamp":1740108332405,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T00:00:00Z","timestamp":1649203200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T00:00:00Z","timestamp":1649203200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s00236-022-00419-z","type":"journal-article","created":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T08:13:55Z","timestamp":1649232835000},"page":"725-759","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Translation validation of coloured Petri net models of programs on integers"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5865-9754","authenticated-orcid":false,"given":"Soumyadip","family":"Bandyopadhyay","sequence":"first","affiliation":[]},{"given":"Dipankar","family":"Sarkar","sequence":"additional","affiliation":[]},{"given":"Chittaranjan","family":"Mandal","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Giese","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,4,6]]},"reference":[{"key":"419_CR1","unstructured":"Coq. https:\/\/coq.inria.fr\/"},{"key":"419_CR2","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/197405.197406","volume":"26","author":"DF Bacon","year":"1994","unstructured":"Bacon, D.F., Graham, S.L., Sharp, O.J.: Compiler transformations for high-performance computing. ACM Comput. Surv. 26, 345\u2013420 (1994)","journal-title":"ACM Comput. Surv."},{"key":"419_CR3","doi-asserted-by":"crossref","unstructured":"Bandyopadhyay, S.: Path based equivalence checking of petri net representation of programs for translation validation. PhD thesis, I.I.T Kharagpur, India, (2016)","DOI":"10.1145\/2856636.2856652"},{"issue":"4","key":"419_CR4","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s00236-018-0320-2","volume":"56","author":"S Bandyopadhyay","year":"2019","unstructured":"Bandyopadhyay, S., Sarkar, D., Mandal, C.: Equivalence checking of petri net models of programs using static and dynamic cut-points. Acta Informatica 56(4), 321\u2013383 (2019)","journal-title":"Acta Informatica"},{"issue":"2","key":"419_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1142\/S0129626416500109","volume":"26","author":"S Bandyopadhyay","year":"2016","unstructured":"Bandyopadhyay, S., Sarkar, D., Mandal, C.A., Banerjee, K., Duddu, K.R.: A path construction algorithm for translation validation using PRES+ models. Parallel Process. Lett. 26(2), 1\u201325 (2016)","journal-title":"Parallel Process. Lett."},{"key":"419_CR6","doi-asserted-by":"crossref","unstructured":"Banerjee, K., Karfa, C., Sarkar, D., Mandal, C.: Verification of code motion techniques using value propagation. IEEE TCAD, 33(8), (2014)","DOI":"10.1109\/TCAD.2014.2314392"},{"issue":"10","key":"419_CR7","doi-asserted-by":"publisher","first-page":"946","DOI":"10.1109\/TSE.2016.2645687","volume":"43","author":"K Banerjee","year":"2017","unstructured":"Banerjee, K., Sarkar, D., Mandal, C.: Deriving bisimulation relations from path extension based equivalence checkers. IEEE Trans. Software Eng. 43(10), 946\u2013953 (2017)","journal-title":"IEEE Trans. Software Eng."},{"key":"419_CR8","doi-asserted-by":"crossref","unstructured":"Bell, C.J.: Certifiably sound parallelizing transformations. In: Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, pages 227\u2013242, (2013)","DOI":"10.1007\/978-3-319-03545-1_15"},{"key":"419_CR9","unstructured":"Bondhugula, U., Hartono, A., Ramanujam, J., Sadayappan, P.: Pluto: A practical and fully automatic polyhedral program optimization system. In: PLDI 08, (2008)"},{"issue":"12\u201315","key":"419_CR10","first-page":"571","volume":"49","author":"LA Cort\u00e9s","year":"2003","unstructured":"Cort\u00e9s, L.A., Eles, P., Peng, Z.: Modeling and formal verification of embedded systems based on a Petri net representation. JSA 49(12\u201315), 571\u2013598 (2003)","journal-title":"JSA"},{"key":"419_CR11","unstructured":"Edwards, S., Lavagno, L., Lee, E.A., Sangiovanni-Vincentellni, A.: Design of embedded systems: Formal models, validation and synthesis. DAC \u201999, pp. 296\u2013299, (1999)"},{"key":"419_CR12","unstructured":"Gupta, S., Dutt, N., Gupta, R., Nicolau, A.: Spark: a high-level synthesis framework for applying parallelizing compiler transformations. In: Proc. of Int. Conf. on VLSI Design, pp. 461\u2013466, Washington, DC, USA, Jan (2003). IEEE Computer Society"},{"issue":"8","key":"419_CR13","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"419_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/b95112","volume-title":"Coloured Petri Nets - Modelling and Validation of Concurrent Systems","author":"K Jensen","year":"2009","unstructured":"Jensen, K., Kristensen, L.M.: Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Springer, Berlin (2009)"},{"issue":"3","key":"419_CR15","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3), 213\u2013254 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"419_CR16","first-page":"30","volume":"17","author":"C Karfa","year":"2012","unstructured":"Karfa, C., Mandal, C., Sarkar, D.: Formal verification of code motion techniques using data-flow-driven equivalence checking. ACM Trans. Design Autom. Electr. Syst. 17(3), 30 (2012)","journal-title":"ACM Trans. Design Autom. Electr. Syst."},{"key":"419_CR17","doi-asserted-by":"crossref","unstructured":"Kundu, S., Lerner, S., Gupta, R.: Validating high-level synthesis. In Proceedings of the 20th international conference on Computer Aided Verification, CAV \u201908, pp. 459\u2013472, Berlin, Heidelberg, (2008). Springer-Verlag","DOI":"10.1007\/978-3-540-70545-1_44"},{"key":"419_CR18","doi-asserted-by":"crossref","unstructured":"Lidman, J., Quinlan, D.J., Liao, C., McKee, S.A.: Rose: Fttransform-a source-to-source translation framework for exascale fault-tolerance research. In: DSN workshop, pp. 1\u20136, (2012)","DOI":"10.1109\/DSNW.2012.6264672"},{"key":"419_CR19","doi-asserted-by":"crossref","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.: Romeo: A parametric model-checker for Petri nets with stopwatches. In: Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, pp. 54\u201357, (2009)","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"419_CR20","volume-title":"Mathematical Theory of Computation","author":"Z Manna","year":"1974","unstructured":"Manna, Z.: Mathematical Theory of Computation. McGraw-Hill Kogakusha, Tokyo (1974)"},{"key":"419_CR21","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., (1989)"},{"key":"419_CR22","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI, pp. 83\u201394, (2000)","DOI":"10.1145\/358438.349314"},{"issue":"6","key":"419_CR23","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1109\/43.31522","volume":"8","author":"PG Paulin","year":"1989","unstructured":"Paulin, P.G., Knight, J.P.: Force-directed scheduling for the behavioural synthesis of asics. IEEE Trans. CAD of ICS 8(6), 661\u2013679 (1989)","journal-title":"IEEE Trans. CAD of ICS"},{"key":"419_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: TACAS, pp. 151\u2013166, (1998)","DOI":"10.1007\/BFb0054170"},{"key":"419_CR25","volume-title":"Principles of Compiler Design","author":"V Raghavan","year":"2010","unstructured":"Raghavan, V.: Principles of Compiler Design. Tata McGraw Hill Education Private Limited, New Delhi (2010)"},{"key":"419_CR26","unstructured":"Rinard, M., Diniz, P.: Credible compilation. Technical Report MIT-LCS-TR-776, MIT, (1999)"},{"issue":"3","key":"419_CR27","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J Sevcik","year":"2013","unstructured":"Sevcik, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM (JACM) 60(3), 22\u201350 (2013)","journal-title":"J. ACM (JACM)"},{"key":"419_CR28","unstructured":"Singh, K.: Construction of Petri net based models for C programs, M.Tech. Dissertation, Dept. of Computer Sc. & Engg., I.I.T., Kharagpur, INDIA. https:\/\/cse.iitkgp.ac.in\/~chitta\/pubs\/rep\/thesisKulwant.pdf, https:\/\/github.com\/soumyadipcsis\/Equivalence-checker\/blob\/master\/thesisKulwant.pdf, May (2016)"},{"key":"419_CR29","doi-asserted-by":"crossref","unstructured":"Smith, M.D., Horowitz, M., Lam, M.S.: Efficient superscalar performance through boosting. In: ASPLOS-V: Proceedings of the fifth international conference on Architectural support for programming languages and operating systems, pp. 248\u2013259, New York, NY, USA, (1992). ACM Press","DOI":"10.1145\/143365.143534"},{"issue":"1","key":"419_CR30","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0022-0000(83)90029-6","volume":"27","author":"I Suzuki","year":"1983","unstructured":"Suzuki, I., Murata, T.: A method for stepwise refinement and abstraction of Petri nets. J. Comput. Syst. Sci. 27(1), 51\u201376 (1983)","journal-title":"J. Comput. Syst. Sci."},{"key":"419_CR31","doi-asserted-by":"crossref","unstructured":"Zhang, J., Cheng, B.H.C.: Model-based development of dynamically adaptive software. In: Proceedings of the 28th International Conference on Software Engineering, ICSE \u201906, pp. 371\u2013380, New York, NY, USA, (2006). ACM","DOI":"10.1145\/1134285.1134337"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-022-00419-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-022-00419-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-022-00419-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T06:08:33Z","timestamp":1666332513000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-022-00419-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,6]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["419"],"URL":"https:\/\/doi.org\/10.1007\/s00236-022-00419-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2022,4,6]]},"assertion":[{"value":"9 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 April 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}