{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T03:40:17Z","timestamp":1775014817083,"version":"3.50.1"},"reference-count":15,"publisher":"Pleiades Publishing Ltd","issue":"1","license":[{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2007,2]]},"DOI":"10.1134\/s0361768807010033","type":"journal-article","created":{"date-parts":[[2007,2,5]],"date-time":"2007-02-05T04:12:56Z","timestamp":1170648776000},"page":"14-23","source":"Crossref","is-referenced-by-count":14,"title":["Verification as a parameterized testing (experiments with the SCP4 supercompiler)"],"prefix":"10.1134","volume":"33","author":[{"given":"A. P.","family":"Lisitsa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. P.","family":"Nemytykh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"137","reference":[{"key":"1003_CR1","unstructured":"Nemytykh, A.P. and Turchin, V.F., The Supercompiler SCP4: Sources, On-Line Demonstration, 2000, http:\/\/www.botik.ru\/pub\/local\/scp\/refal5\/."},{"key":"1003_CR2","first-page":"162","volume":"2890","author":"A.P. Nemytykh","year":"2003","unstructured":"Nemytykh, A.P., The Supercompiler SCP4: General Structure (Extended Abstract), Lecture Notes in Computer Science (Proc. of the 5th Int. Conf. Perspectives of System Informatics), 2003, vol. 2890, pp. 162\u2013170, http:\/\/www.botik.ru\/pub\/local\/scp\/refal5\/nemytykh_PSI03.ps.gz.","journal-title":"Lecture Notes in Computer Science (Proc. of the 5th Int. Conf. Perspectives of System Informatics)"},{"key":"1003_CR3","first-page":"53","volume":"1855","author":"G. Delzanno","year":"2003","unstructured":"Delzanno, G., Automatic Verification of Parameterized Cache Coherence Protocols, Lecture Notes in Computer Science (Proc. 12th Int. Conf. Computer Aided Verification), 2003, vol. 1855, pp. 53\u201368.","journal-title":"Lecture Notes in Computer Science (Proc. 12th Int. Conf. Computer Aided Verification)"},{"key":"1003_CR4","unstructured":"Delzanno, G., Automatic Verification of Cache Coherence Protocols via Infinite-state Constraint-based Model Checking, http:\/\/www.disi.unige.it\/person\/DelzannoG\/protocol.html."},{"key":"1003_CR5","volume-title":"Refal-5, Programming Guide and Reference Manual","author":"V.F. Turchin","year":"1989","unstructured":"Turchin, V.F., Refal-5, Programming Guide and Reference Manual, Holyoke, MA: New England, 1989, http:\/\/www.botik.ru\/pub\/local\/scp\/refal5\/."},{"key":"1003_CR6","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/5956.5957","volume":"8","author":"V.F. Turchin","year":"1986","unstructured":"Turchin, V.F., The Concept of a Supercompiler, ACM Trans. Programming Languages Systems, 1986, vol. 8, pp. 292\u2013325.","journal-title":"ACM Trans. Programming Languages Systems"},{"key":"1003_CR7","unstructured":"Turchin, V.F., Turchin, D.V., Konyshev, A.P., and Nemytykh, A.P., Refal-5, Sources, Executable Modules, 2000, http:\/\/www.botik.ru\/pub\/local\/scp\/refal5\/."},{"key":"1003_CR8","first-page":"448","volume":"1","author":"A.P. Nemytykh","year":"2004","unstructured":"Nemytykh, A.P., The Supercompiler SCP4: General Structure, Programmnye System: Teoriya i Primenenie, 2004, vol. 1, pp. 448\u2013485, ftp:\/\/ftp.botik.ru\/pub\/local\/scp\/refal5\/GenStruct.ps.gz\".","journal-title":"Programmnye System: Teoriya i Primenenie"},{"key":"1003_CR9","doi-asserted-by":"crossref","unstructured":"Bundy, A., The Automation of Proof by Mathematical Induction, in Handbook of Automated Reasoning, 2001, pp. 845\u2013911.","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"1003_CR10","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Verification of Consistency Protocols via Infinite-State Symbolic Model Checking: A Case Study, Proc. of FORTE\/PSTV, 2000, pp. 171\u2013188.","DOI":"10.1007\/978-0-387-35533-7_11"},{"key":"1003_CR11","unstructured":"Korlyukov, A.V., Manual on the SCP4 Supercompiler, 1999, http:\/\/www.refal.net\/supercom.htm."},{"key":"1003_CR12","first-page":"123","volume":"1","author":"A.V. Korlyukov","year":"2004","unstructured":"Korlyukov, A.V. and Nemytykh, A.P., Supercompilation of Double Interpretation (How One Hour of the Machine\u2019s Time Can Be Turned to One Second), Vestn. natsional\u2019nogo tekh. univ. Khar\u2019kovskogo politekhnicheskogo inst., 2004, vol. 1, pp. 123\u2013150, http:\/\/www.refal.net\/korlukov\/scp2int\/Karliukou_Nemytykh.pdf. Sources and demonstration, 2002: http:\/\/www.refal.net\/:_korlukov\/demo_scp4xslt.zip.","journal-title":"Vestn. natsional\u2019nogo tekh. univ. Khar\u2019kovskogo politekhnicheskogo inst."},{"key":"1003_CR13","doi-asserted-by":"publisher","first-page":"210","DOI":"10.2307\/1993287","volume":"95","author":"J.B. Kruskal","year":"1960","unstructured":"Kruskal, J.B., Well-Quasi-Ordering, the Tree Theorem, and Vaszonyi\u2019s Conjecture, Trans. AMS, 1960, vol. 95, pp. 210\u2013225.","journal-title":"Trans. AMS"},{"key":"1003_CR14","first-page":"199","volume":"1559","author":"M. Leuschel","year":"1998","unstructured":"Leuschel, M., Improving Homeomorphic Embedding for Online Termination, Lecture Notes in Computer Science (Proc. 8th Int. Workshop on Logic Program Synthesis and Transformation (LOPSTR)), 1998, vol. 1559, pp. 199\u2013218.","journal-title":"Lecture Notes in Computer Science (Proc. 8th Int. Workshop on Logic Program Synthesis and Transformation (LOPSTR))"},{"key":"1003_CR15","volume-title":"Proc. Third Workshop on Applied Semantics (APPSEM05)","author":"A. Lisitsa","year":"2005","unstructured":"Lisitsa, A. and Nemytykh, A.P., Verification of Parameterized Systems Using Supercompilation. A Case Study, Proc. Third Workshop on Applied Semantics (APPSEM05), Hofmann, M. and Loidl, H.W., Eds., Ludwig Maximillians Universit\u00e4t Munchen, Fraunchiemsee, Germany, 2005, ftp:\/\/www.botik.ru\/pub\/local\/scp\/refal5\/appsem_verification2005.ps."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768807010033.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768807010033","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768807010033","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768807010033.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:22:11Z","timestamp":1775010131000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768807010033"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2]]}},"alternative-id":["1003"],"URL":"https:\/\/doi.org\/10.1134\/s0361768807010033","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}