乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:45:45Z","timestamp":1725558345282},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405245"},{"type":"electronic","value":"9783540450696"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45069-6_2","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T17:11:46Z","timestamp":1277226706000},"page":"14-26","source":"Crossref","is-referenced-by-count":69,"title":["Bounded Model Checking and Induction: From Refutation to Verification"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[]},{"given":"Maria","family":"Sorea","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., Bjesse, P., E\u00e9n, N.: Symbolic reachability analysis based on SAT-solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 411\u2013425. Springer, Heidelberg (2000)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 8\u201322. Springer, Heidelberg (1999)"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Formal Methods in System Design\u00a015, 75\u201392 (1999)","journal-title":"Formal Methods in System Design"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zh, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"2_CR6","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on demand for satisfiability solvers. Annals of Mathematics and Artificial Intelligence (2002) (Accepted for publication)"},{"key":"2_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","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.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated Canonization and Solving. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"issue":"1","key":"2_CR10","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/TSE.1975.6312821","volume":"1","author":"S.M. German","year":"1975","unstructured":"German, S.M., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Transactions on Software Engineering\u00a01(1), 68\u201375 (1975)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR11","first-page":"500","volume-title":"Proceedings of the 3rd IJCAI","author":"S.M. Katz","year":"1973","unstructured":"Katz, S.M., Manna, Z.: A heuristic approach to program verification. In: Nilsson, N.J. (ed.) Proceedings of the 3rd IJCAI, Stanford, CA, pp. 500\u2013512. William Kaufmann, San Francisco (1973)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Kroening","year":"2002","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 298\u2013309. Springer, Heidelberg (2002)"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design\u00a06(1), 11\u201344 (1995)","journal-title":"Formal Methods in System Design"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"2002","unstructured":"McMillan, K.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 250. Springer, Heidelberg (2002)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-52148-8_30","volume-title":"Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1990","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines using symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 365\u2013373. Springer, Heidelberg (1990)"},{"key":"2_CR16","unstructured":"Rushby, J.: Model checking Simpson\u2019s four-slot fully asynchronous communication mechanism. Technical report, CSL, SRI International, Menlo Park, Menlo Park, CA (July 2002)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"issue":"1","key":"2_CR18","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1049\/ip-e.1990.0002","volume":"137","author":"H.R. Simpson","year":"1990","unstructured":"Simpson, H.R.: Four-slot fully asynchronous communication mechanism. IEE Proceedings, Part E: Computers and Digital Techniques\u00a0137(1), 17\u201330 (1990)","journal-title":"IEE Proceedings, Part E: Computers and Digital Techniques"},{"key":"2_CR19","unstructured":"Sorea, M.: Bounded model checking for timed automata. In: Proceedings of MTCS 2002. Electronic Notes in Theoretical Computer Science, vol.\u00a068 (2002)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_13","volume-title":"Computer Aided Verification","author":"P.F. Williams","year":"2000","unstructured":"Williams, P.F., Biere, A., Clarke, E.M., Gupta, A.: Combining decision diagrams and SAT procedures for efficient symbolic model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45069-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T16:53:56Z","timestamp":1580316836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45069-6_2"}},"subtitle":["(Extended Abstract, Category A)"],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405245","9783540450696"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45069-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}