{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:30Z","timestamp":1762458570876},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_25","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"362-378","source":"Crossref","is-referenced-by-count":17,"title":["Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]},{"given":"Enrica","family":"Nicolini","sequence":"additional","affiliation":[]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[]},{"given":"Daniele","family":"Zucchelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_42","volume-title":"Automated Reasoning","author":"M.P. Bonacina","year":"2006","unstructured":"Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification of infinite state structures. In: Handbook of Process Algebras (2001)","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"25_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"25_CR4","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Demri, S.: Linear-time temporal logics with Presburger constraints: An overview. Journal of Applied Non-Classical Logics 16(3-4) (2006)","DOI":"10.3166\/jancl.16.311-347"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11901914_36","volume-title":"Automated Technology for Verification and Analysis","author":"S. Demri","year":"2006","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Towards a model-checker for counter systems. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, Springer, Heidelberg (2006)"},{"key":"25_CR7","unstructured":"Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications. North-Holland Publishing Co. (2003)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning 33(3-4) (2004)","DOI":"10.1007\/s10817-004-6241-5"},{"key":"25_CR9","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. Technical Report RI313-07, Universit\u00e0 degli Studi di Milano (2007), Available at http:\/\/homes.dsi.unimi.it\/~zucchell\/publications\/techreport\/GhiNiRaZu-RI313-07.pdf"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"M. Maidl","year":"2001","unstructured":"Maidl, M.: A unifying model checking approach for safety properties of parameterized systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"25_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Minsky, M.L.: Recursive unsolvability of Post\u2019s problem of \u201ctag\u201d and other topics in the theory of Turing machines. Annals of Mathematics 74(3) (1961)","DOI":"10.2307\/1970290"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transaction on Programming Languages and Systems 1(2) (1979)","DOI":"10.1145\/357073.357079"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Plaisted, D.A.: A decision procedure for combination of propositional temporal logic and other specialized theories. Journal of Automated Reasoning 2(2) (1986)","DOI":"10.1007\/BF02432150"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruath, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, Springer, Heidelberg (2001)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Formal Methods in System Design 15(1) (1999)","DOI":"10.1023\/A:1008791913551"},{"key":"25_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_21","volume-title":"Automated Reasoning","author":"V. Sofronie-Stokkermans","year":"2006","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proc. of FroCoS 1996 (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Verification of concurrent programs: the automata-theoretic framework. Annals of Pure and Applied Logic 51(1-2) (1991)","DOI":"10.1016\/0168-0072(91)90066-U"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:06Z","timestamp":1619517186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}