{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:53:12Z","timestamp":1773654792659,"version":"3.50.1"},"reference-count":17,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2008,8]]},"abstract":"<jats:p> We present an approach to verification of parameterized systems, which is based on program transformation technique known as supercompilation. In this approach the statements about safety properties of a system to be verified are translated into the statements about properties of the program that simulates and tests the system. Supercompilation is used then to establish the required properties of the program. In this paper we show that reachability analysis performed by supercompilation can be seen as the proof of a correctness condition by induction. We formulate suitable induction principles and proof strategies and illustrate their use by examples of verification of parameterized protocols. <\/jats:p>","DOI":"10.1142\/s0129054108006066","type":"journal-article","created":{"date-parts":[[2008,8,6]],"date-time":"2008-08-06T06:30:40Z","timestamp":1218004240000},"page":"953-969","source":"Crossref","is-referenced-by-count":15,"title":["REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION"],"prefix":"10.1142","volume":"19","author":[{"given":"ALEXEI","family":"LISITSA","sequence":"first","affiliation":[{"name":"Department of Computer Science, The University of Liverpool, Ashton Building, Liverpool L69 3BX, United Kingdom"}]},{"given":"ANDREI P.","family":"NEMYTYKH","sequence":"additional","affiliation":[{"name":"Program Systems Institute, Russian Academy of Sciences, Pereslavl-Zalessky,  Yaroslavl region 152020, Russia"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf2","first-page":"1","volume":"50","author":"Baukus K.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"rf4","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999"},{"key":"rf8","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026276129010"},{"key":"rf9","first-page":"19","volume":"4","author":"Ershov A. P.","journal-title":"Acta Cybernetica"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050074"},{"key":"rf14","first-page":"326","volume":"2","author":"Higman G.","journal-title":"Proc. London Math. Soc."},{"key":"rf15","volume-title":"Partial Evaluation and Automatic Program Generation","author":"Jones N. D.","year":"1993"},{"key":"rf17","first-page":"210","volume":"95","author":"Kruskal J. B.","journal-title":"Trans. Amer. Math. Society"},{"key":"rf25","first-page":"22","volume":"1","author":"Lisitsa A. P.","journal-title":"Programmirovanie"},{"key":"rf32","unstructured":"A. P.\u00a0Nemytykh, Programmnye sistemy: teoriya i prilozheniya\u00a01 (Fizmatlit, Moscow, 2004)\u00a0pp. 448\u2013485,\u00a0ftp:\/\/ftp.botik.ru\/pub\/local\/scp\/refal5\/GenStruct.ps.gz."},{"key":"rf33","volume-title":"The Supercompiler SCP4'- General Structure","author":"Nemytykh A. P.","year":"2007"},{"key":"rf36","unstructured":"A.\u00a0Roychoudhury and C. R.\u00a0Ramakrishnan, Program Development in Computational Logic, LNCS\u00a03049 (2004)\u00a0pp. 262\u2013291."},{"key":"rf37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59293-8_228"},{"key":"rf40","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800002008"},{"key":"rf41","doi-asserted-by":"publisher","DOI":"10.1145\/5956.5957"},{"key":"rf43","volume-title":"Refal-5, Programming Guide and Reference Manual","author":"Turchin V. F.","year":"1989"},{"key":"rf46","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90147-A"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054108006066","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T11:24:04Z","timestamp":1565177044000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054108006066"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,8]]},"references-count":17,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2008,8]]}},"alternative-id":["10.1142\/S0129054108006066"],"URL":"https:\/\/doi.org\/10.1142\/s0129054108006066","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,8]]}}}