{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:21:28Z","timestamp":1775053288283,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642297083","type":"print"},{"value":"9783642297090","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29709-0_18","type":"book-chapter","created":{"date-parts":[[2012,5,12]],"date-time":"2012-05-12T09:49:34Z","timestamp":1336816174000},"page":"193-209","source":"Crossref","is-referenced-by-count":4,"title":["Solving Coverability Problem for Monotonic Counter Systems by Supercompilation"],"prefix":"10.1007","author":[{"given":"Andrei V.","family":"Klimov","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 27-30, pp. 313\u2013321. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"5","key":"18_CR2","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S. Bardin","year":"2008","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. International Journal on Software Tools for Technology Transfer\u00a010(5), 401\u2013424 (2008)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BFb0055044","volume-title":"Automata, Languages and Programming","author":"C. Dufourd","year":"1998","unstructured":"Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets Between Decidability and Undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 103\u2013115. Springer, Heidelberg (1998)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/3-540-56689-9_45","volume-title":"Advances in Petri Nets 1993","author":"A. Finkel","year":"1993","unstructured":"Finkel, A.: The Minimal Coverability Graph for Petri Nets. In: Rozenberg, G. (ed.) APN 1993. LNCS, vol.\u00a0674, pp. 210\u2013243. Springer, Heidelberg (1993)"},{"key":"18_CR5","unstructured":"Geeraerts, G.: Coverability and Expressiveness Properties of Well-Structured Transition Systems. PhD thesis, Universit\u00e9 Libre de Bruxelles, Belgique (May 2007), http:\/\/www.ulb.ac.be\/di\/verif\/ggeeraer\/thesis.pdf"},{"issue":"1","key":"18_CR6","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.jcss.2005.09.001","volume":"72","author":"G. Geeraerts","year":"2006","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences\u00a072(1), 180\u2013203 (2006)","journal-title":"Journal of Computer and System Sciences"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-540-75596-8_9","volume-title":"Automated Technology for Verification and Analysis","author":"G. Geeraerts","year":"2007","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the Efficient Computation of the Minimal Coverability Set for Petri Nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 98\u2013113. Springer, Heidelberg (2007)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-46562-6_8","volume-title":"Perspectives of System Informatics","author":"R. Gl\u00fcck","year":"2000","unstructured":"Gl\u00fcck, R., Leuschel, M.: Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol.\u00a01755, pp. 93\u2013100. Springer, Heidelberg (2000)"},{"issue":"2","key":"18_CR9","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci.\u00a03(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"18_CR10","first-page":"43","volume-title":"Proceedings of the First International Workshop on Metacomputation in Russia","author":"A.V. Klimov","year":"2008","unstructured":"Klimov, And.V.: An approach to supercompilation for object-oriented languages: the Java Supercompiler case study. In: Nemytykh, A.P. (ed.) Proceedings of the First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp. 43\u201353. Ailamazyan University of Pereslavl, Pereslavl-Zalessky (2008)"},{"key":"18_CR11","unstructured":"Klimov, And.V.: JVer Project: Verification of Java programs by Java Supercompiler (2008), http:\/\/pat.keldysh.ru\/jver\/"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-11486-1_16","volume-title":"Perspectives of Systems Informatics","author":"A.V. Klimov","year":"2010","unstructured":"Klimov, And.V.: A Java Supercompiler and Its Application to Verification of Cache-Coherence Protocols. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol.\u00a05947, pp. 185\u2013192. Springer, Heidelberg (2010)"},{"key":"18_CR13","unstructured":"Klimov, And.V.: Yet another algorithm for solving coverability problem for monotonic counter systems. In: Nepomnyaschy, V., Sokolov, V. (eds.) Second Workshop on Program Semantics, Specification and Verification: Theory and Applications, PSSV 2011, St. Petersburg, Russia, June 12-13, pp. 59\u201367. Yaroslavl State University (2011)"},{"key":"18_CR14","unstructured":"Klyuchnikov, I.: Supercompiler HOSC 1.1: proof of termination. Preprint\u00a021, Keldysh Institute of Applied Mathematics, Moscow (2010)"},{"key":"18_CR15","series-title":"LNCS","first-page":"210","volume-title":"PSI 2011","author":"I. Klyuchnikov","year":"2012","unstructured":"Klyuchnikov, I., Romanenko, S.: Multi-result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol.\u00a07162, pp. 210\u2013226. Springer, Heidelberg (2012)"},{"key":"18_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-44957-4_7","volume-title":"Computational Logic - CL 2000","author":"M. Leuschel","year":"2000","unstructured":"Leuschel, M., Lehmann, H.: Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 101\u2013115. Springer, Heidelberg (2000)"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Lehmann, H.: Solving coverability problems of Petri nets by partial deduction. In: Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Montreal, Canada, September 20-23, pp. 268\u2013279. ACM (2000)","DOI":"10.1145\/351268.351298"},{"key":"18_CR18","unstructured":"Lisitsa, A.P., Nemytykh, A.P.: Solving coverability problems by supercompilation. Invited talk. In: The Second Workshop on Reachability Problems in Computational Models (RP 2008), Liverpool, UK, September 15-17 (2008)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Lisitsa, A.P., Nemytykh, A.P.: Towards verification via supercompilation. In: COMPSAC (2), pp. 9\u201310. IEEE Computer Society (2005)","DOI":"10.1109\/COMPSAC.2005.159"},{"key":"18_CR20","unstructured":"Lisitsa, A.P., Nemytykh, A.P.: Experiments on verification via supercompilation (2007), http:\/\/refal.botik.ru\/protocols\/"},{"issue":"1","key":"18_CR21","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1134\/S0361768807010033","volume":"33","author":"A.P. Lisitsa","year":"2007","unstructured":"Lisitsa, A.P., Nemytykh, A.P.: Verification as a parameterized testing (experiments with the SCP4 supercompiler). Programming and Computer Software\u00a033(1), 14\u201323 (2007)","journal-title":"Programming and Computer Software"},{"issue":"4","key":"18_CR22","doi-asserted-by":"publisher","first-page":"953","DOI":"10.1142\/S0129054108006066","volume":"19","author":"A.P. Lisitsa","year":"2008","unstructured":"Lisitsa, A.P., Nemytykh, A.P.: Reachability analysis in verification via supercompilation. Int. J. Found. Comput. Sci.\u00a019(4), 953\u2013969 (2008)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"18_CR23","unstructured":"Luttge, K.: Zustandsgraphen von Petri-Netzen. Master\u2019s thesis, Humboldt-Universit\u00e4t zu Berlin, Germany (1995)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-39866-0_18","volume-title":"Perspectives of System Informatics","author":"A.P. Nemytykh","year":"2004","unstructured":"Nemytykh, A.P.: The Supercompiler SCP4: General Structure. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol.\u00a02890, pp. 162\u2013170. Springer, Heidelberg (2004)"},{"key":"18_CR25","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: An algorithm of generalization in positive supercompilation. In: Lloyd, J.W. (ed.) International Logic Programming Symposium, Portland, Oregon, December 4-7, pp. 465\u2013479. MIT Press (1995)"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/3-540-10003-2_105","volume-title":"Automata, Languages and Programming","author":"V.F. Turchin","year":"1980","unstructured":"Turchin, V.F.: The Use of Metasystem Transition in Theorem Proving and Program Optimization. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 645\u2013657. Springer, Heidelberg (1980)"},{"issue":"3","key":"18_CR27","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. Transactions on Programming Languages and Systems\u00a08(3), 292\u2013325 (1986)","journal-title":"Transactions on Programming Languages and Systems"},{"key":"18_CR28","unstructured":"Turchin, V.F.: The algorithm of generalization in the supercompiler. In: Bj\u00f8rner, D., Ershov, A.P., Jones, N.D. (eds.) Partial Evaluation and Mixed Computation, pp. 531\u2013549. North-Holland (1988)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of Systems Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29709-0_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:56:46Z","timestamp":1743112606000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29709-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642297083","9783642297090"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29709-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}