{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:41:19Z","timestamp":1725565279007},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223818"},{"type":"electronic","value":"9783540278153"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27815-3_11","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:32:16Z","timestamp":1284438736000},"page":"87-101","source":"Crossref","is-referenced-by-count":0,"title":["Model-Checking Systems with Unbounded Variables without Abstraction"],"prefix":"10.1007","author":[{"given":"Magali","family":"Contensin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurence","family":"Pierre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031810","volume-title":"Formal Methods in Computer-Aided Design","author":"R. Hojati","year":"1996","unstructured":"Hojati, R., Isles, A., Kirkpatrick, D., Brayton, R.: Verification using Uninterpreted Functions and Finite Instantiations. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, Springer, Heidelberg (1996)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-49519-3_24","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Berezin","year":"1998","unstructured":"Berezin, S., Biere, A., Clarke, E., Zhu, Y.: Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 369\u2013386. Springer, Heidelberg (1998)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Browne, A., Col\u00f3n, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods in System Design\u00a016 (2000)","DOI":"10.1023\/A:1008700623084"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Symposium on Principles of Programming Languages (2002)","DOI":"10.1145\/503272.503279"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Du, X., Ramakrishnan, C., Smolka, S.: Real-Time Verification Techniques for Untimed Systems. Electronic Notes in Theoretical Computer Science 39 (2000)","DOI":"10.1016\/S1571-0661(05)80751-0"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Peled, D.: Combining Partial Order Reductions with On-the-Fly Model-Checking. Formal Methods in System Design 8 (1996)","DOI":"10.1007\/BF00121262"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Naumovich, G., Clarke, L., Cobleigh, J.: Using partial order techniques to improve performance of data flow analysis based verification. In: Workshop on Program Analysis For Software Tools and Engineering (1999)","DOI":"10.1145\/316158.316180"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-44585-4_9","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Sistla, P.: Symmetry and reduced symmetry in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 91. Springer, Heidelberg (2001)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Uribe, T.E.: Combinations of model checking and theorem proving. In: Frontiers of Combining Systems, pp. 151\u2013170 (2000)","DOI":"10.1007\/10720084_11"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031809","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Schneider","year":"1996","unstructured":"Schneider, K., Kropf, T.: A unified approach for combining different formalisms for hardware verification. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, Springer, Heidelberg (1996)"},{"key":"11_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Pub, Dordrecht (1993)"},{"volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","year":"1993","key":"11_CR13","unstructured":"Gordon, M., Melham, T. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Proc. Computer Aided Verification, pp. 312\u2013327 (2000)","DOI":"10.1007\/10722167_25"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Contensin, M., Pierre, L.: Combining ACL2 and a \u03bd-calculus Model-checker to Verify System-level Designs. In: Proc. ACM & IEEE International Conference MEMOCODE 2003 (2003)","DOI":"10.1109\/MEMCOD.2003.1210091"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Winskel, G.: A note on model-checking the modal \u03bd-calculus. Theoretical Computer Science\u00a083 (1991)","DOI":"10.1016\/0304-3975(91)90043-2"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027 (1983)","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"11_CR18","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Dordrecht (2000)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44618-4_1","volume-title":"CONCUR 2000 - Concurrency Theory","author":"N. Shankar","year":"2000","unstructured":"Shankar, N.: Combining Theorem Proving and Model Checking through Symbolic Analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, p. 1. Springer, Heidelberg (2000)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013237. Springer, Heidelberg (1999)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/BFb0028771","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: InVeSt: A tool for the verification of invariants. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 505\u2013510. Springer, Heidelberg (1998)"},{"key":"11_CR23","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Proc. Workshop on Industrial-Strength Formal Specification Techniques (1995)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48683-6_32","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"1999","unstructured":"Manolios, P., Namjoshi, K., Sumners, R.: Linking Theorem Proving and Model- Checking with Well-Founded Bisimulation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 369\u2013379. Springer, Heidelberg (1999)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031813","volume-title":"Formal Methods in Computer-Aided Design","author":"N. Shankar","year":"1996","unstructured":"Shankar, N.: PVS: Combining specification, proof checking and model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, Springer, Heidelberg (1996)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Saidi","year":"1999","unstructured":"Saidi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-48256-3_17","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Schneider","year":"1999","unstructured":"Schneider, K., Hoffmann, D.W.: A HOL conversion for translating linear time temporal logic to \u03c9-automata. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, p. 255. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27815-3_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:22:26Z","timestamp":1605759746000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27815-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223818","9783540278153"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27815-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}