{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T22:10:05Z","timestamp":1745964605612,"version":"3.40.4"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,2,23]],"date-time":"2013-02-23T00:00:00Z","timestamp":1361577600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1007\/s10817-013-9274-9","type":"journal-article","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T03:55:18Z","timestamp":1361505318000},"page":"431-451","source":"Crossref","is-referenced-by-count":3,"title":["Finite Reasons for Safety"],"prefix":"10.1007","volume":"51","author":[{"given":"Alexei","family":"Lisitsa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,2,23]]},"reference":[{"issue":"2","key":"9274_CR1","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"PA Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91\u2013101 (1996)","journal-title":"Inf. Comput."},{"issue":"5","key":"9274_CR2","doi-asserted-by":"crossref","first-page":"779","DOI":"10.1142\/S0129054109006887","volume":"20","author":"PA Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Monotonic abstraction: on efficient verification of parameterized systems. Int. J. Found. Comput. Sci. 20(5), 779\u2013801 (2009)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"9274_CR3","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-642-02138-1_3","volume":"5522","author":"PA Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno G., Rezine, A.: Approximated context-sensitive analysis for parameterized verification. Lect. Notes Comput. Sci. 5522, 41\u201356 (2009)","journal-title":"Lect. Notes Comput. Sci."},{"issue":"9","key":"9274_CR4","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.1016\/j.jsc.2011.12.031","volume":"47","author":"P Baumgartner","year":"2012","unstructured":"Baumgartner, P., Pelzer, B., Tinelli, C.: Model evolution with equality\u2014revised and implemented. J. Symb. Comput. 47(9), 1011\u20131045 (2012)","journal-title":"J. Symb. Comput."},{"key":"9274_CR5","doi-asserted-by":"crossref","unstructured":"Caferra, R., Leitsch, A., Peltier, M.: Automated model building. In: Applied Logic Series, vol. 31. Kluwer (2004)","DOI":"10.1007\/978-1-4020-2653-9"},{"key":"9274_CR6","unstructured":"Comon, H.: Inductionless induction. In: David, R. (ed.) 2nd Int. Conf. in Logic for Computer Science: Automated Deduction. Lecture Notes. Uni de Savoie, Chambery (1994)"},{"issue":"3","key":"9274_CR7","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based verification of parametrized cache coherence protocols. Formal Methods Syst. Des. 23(3), 257\u2013301 (2003)","journal-title":"Formal Methods Syst. Des."},{"key":"9274_CR8","unstructured":"Enderton, H.: A Mathematical Introduction to Logic. Academic Press (1972)"},{"key":"9274_CR9","doi-asserted-by":"crossref","unstructured":"Fisman, D., Pnueli, A.: Beyond regular model checking. In: Proc. of FSTTCS\u201901. LNCS, vol. 2245 (2001)","DOI":"10.1007\/3-540-45294-X_14"},{"key":"9274_CR10","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume":"6173","author":"S Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. Lect. Notes Comput. Sci. 6173, 22\u201329 (2010)","journal-title":"Lect. Notes Comput. Sci."},{"key":"9274_CR11","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Nikolini, E., Ranise, S., Zucchelli, D.: Towards SMT model-checking of array-based systems. In: IJCAR, LNCS (2008)","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"9274_CR12","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq, J.: Towards producing formally checkable security proofs, automatically. In: Computer Security Foundations (CSF), pp. 224\u2013238 (2008)","DOI":"10.1109\/CSF.2008.21"},{"issue":"6","key":"9274_CR13","doi-asserted-by":"crossref","first-page":"1247","DOI":"10.3233\/JCS-2009-0395","volume":"18","author":"J Goubault-Larrecq","year":"2010","unstructured":"Goubault-Larrecq, J.: Finite models for formal security proofs. J. Comput. Secur. 18(6), 1247\u20131299 (2010)","journal-title":"J. Comput. Secur."},{"key":"9274_CR14","doi-asserted-by":"crossref","unstructured":"Guttman, J.: Security theorems via model theory. In: Proceedings 16th International Workshop on Expressiveness in Concurrency, EXPRESS, EPTCS, vol. 8 (2009)","DOI":"10.4204\/EPTCS.8.5"},{"issue":"3","key":"9274_CR15","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/j.entcs.2005.01.044","volume":"138","author":"P Habermehl","year":"2005","unstructured":"Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. Electron. Notes Theor. Comput. Sci. (ENTCS) 138(3), 21\u201336 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci. (ENTCS)"},{"key":"9274_CR16","doi-asserted-by":"crossref","unstructured":"Jurjens, J., Weber, T.: Finite models in FOL-based crypto-protocol verification. In: Degano, P., Vigan\u00f2, L. (eds.) ARSPA-WITS 2009, LNCS 5511, pp.\u00a0155\u2013172 (2009)","DOI":"10.1007\/978-3-642-03459-6_11"},{"key":"9274_CR17","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R.: Proof by consistency. Artif. Intell. 31, 125\u2013157 (1987)","journal-title":"Artif. Intell."},{"key":"9274_CR18","unstructured":"Lallement, G.: Semigroups and Combinatorial Applications. Wiley (1979)"},{"key":"9274_CR19","unstructured":"Lisitsa, A.: Verfication via countermodel finding. http:\/\/www.csc.liv.ac.uk\/~alexei\/countermodel"},{"key":"9274_CR20","unstructured":"Lisitsa, A.: Reachability as deducibility, finite countermodels and verification. In: Preproceedings of AVOCS 2009, Technical Report of Computer Science, Swansea University, CSR-2-2009, pp.\u00a0241\u2013243 (2009)"},{"key":"9274_CR21","doi-asserted-by":"crossref","unstructured":"Lisitsa, A.: Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol. In: Proceedings of WING 2010, 1\u00a0pp. (2010)","DOI":"10.29007\/gt85"},{"key":"9274_CR22","doi-asserted-by":"crossref","unstructured":"Lisitsa, A.: Reachability as deducibility, finite countermodels and verification. In: Proceedings of ATVA 2010. LNCS, vol. 6252, pp. 233\u2013244 (2010)","DOI":"10.1007\/978-3-642-15643-4_18"},{"key":"9274_CR23","unstructured":"Lisitsa, A.: Finite model finding for parameterized verification. CoRR arXiv:1011.0047 (2010). Accessed 12 Feb 2013"},{"key":"9274_CR24","unstructured":"Lisitsa, A.: Finite countermodels for safety verification of parameterized tree systems. CoRR arXiv:1107.5142 . Accessed 12 Feb 2013"},{"key":"9274_CR25","unstructured":"Lisitsa, A.: Finite models vs tree automata in safety verification. In: 23rd International Conference on Rewriting Techniques and Applications RTA\u201912, pp. 225\u2013239 (2012)"},{"key":"9274_CR26","unstructured":"McCune, W.: Prover9 and Mace4. http:\/\/www.cs.unm.edu\/~mccune\/mace4 . Accessed 12 Feb 2013"},{"key":"9274_CR27","unstructured":"Nilsson, M.: Regular model checking. Acta Universitatis Upsaliensis. Uppsala Dissertations from the Faculty of Science and Technology 60. 149\u00a0pp. Uppsala. ISBN 91-554-6137-9 (2005)"},{"key":"9274_CR28","doi-asserted-by":"crossref","unstructured":"Nonnengart, A.: Hybrid systems verification by location elimination. In: Lynch, N.A., Krogh, B.H. (eds.) Hybrid Systems: Computation and Control, Third International Workshop, HSCC 2000, LNCS, vol.\u00a01790, pp.\u00a0352\u2013365 (2000)","DOI":"10.1007\/3-540-46430-1_30"},{"issue":"1","key":"9274_CR29","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S1571-0661(04)00245-2","volume":"55","author":"P Selinger","year":"2001","unstructured":"Selinger, P.: Models for an adversary-centric protocol logic. Electron. Notes Theor. Comput. Sci. 55(1), 69\u201384 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9274_CR30","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.): CADE-16, LNAI, vol. 1632, pp.\u00a0314\u2013328 (1999)","DOI":"10.1007\/3-540-48660-7_29"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9274-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9274-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9274-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:56:19Z","timestamp":1745963779000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9274-9"}},"subtitle":["Parameterized Verification by Finite Model Finding"],"short-title":[],"issued":{"date-parts":[[2013,2,23]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["9274"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9274-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2013,2,23]]}}}