乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:08:46Z","timestamp":1725746926546},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319024431"},{"type":"electronic","value":"9783319024448"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-02444-8_12","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T05:11:21Z","timestamp":1377753081000},"page":"148-162","source":"Crossref","is-referenced-by-count":5,"title":["A Framework for Ranking Vacuity Results"],"prefix":"10.1007","author":[{"given":"Shoham","family":"Ben-David","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Computer Aided Verification","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.Y.: Enhanced vacuity detection in linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 368\u2013380. Springer, Heidelberg (2003)"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods in System Design\u00a018(2), 141\u2013162 (2001)","journal-title":"Formal Methods in System Design"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-540-74407-8_33","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"S. Ben-David","year":"2007","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: Temporal antecedent failure: Refining vacuity. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 492\u2013506. Springer, Heidelberg (2007)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/11560548_16","volume-title":"Correct Hardware Design and Verification Methods","author":"D. Bustan","year":"2005","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 191\u2013206. Springer, Heidelberg (2005)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-71289-3_27","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Chechik","year":"2007","unstructured":"Chechik, M., Gheorghiu, M., Gurfinkel, A.: Finding environment guarantees. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol.\u00a04422, pp. 352\u2013367. Springer, Heidelberg (2007)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Chockler, H., Gurfinkel, A., Strichman, O.: Beyond vacuity: Towards the strongest passing formula. In: FMCAD, pp. 1\u20138 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.28"},{"key":"12_CR7","unstructured":"Chockler, H., Halpern, J.Y.: Responsibility and blame: a structural-model approach. In: Proc. 19th IJCAI, pp. 147\u2013153 (2003)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Chockler, H., Strichman, O.: Easier and more informative vacuity checks. In: Proc. 5th MEMOCODE, pp. 189\u2013198 (2007)","DOI":"10.1109\/MEMCOD.2007.371225"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/3-540-58043-3_19","volume-title":"A Decade of Concurrency","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.: Verification tools for finite-state concurrent systems. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol.\u00a0803, pp. 124\u2013175. Springer, Heidelberg (1994)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: Proc. 32st DAC, pp. 427\u2013432. IEEE Computer Society (1995)","DOI":"10.1145\/217474.217565"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM\u00a042, 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"12_CR12","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property pattern mappings for LTL, \n \n http:\/\/patterns.projects.cis.ksu.edu\/documentation\/patterns\/ltl.shtml"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: FMSP, pp. 7\u201315 (1998)","DOI":"10.1145\/298595.298598"},{"issue":"1","key":"12_CR14","first-page":"50","volume":"41","author":"R. Fagin","year":"1976","unstructured":"Fagin, R.: Probabilities in finite models. JSL\u00a041(1), 50\u201358 (1976)","journal-title":"JSL"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"Hardware and Software: Verification and Testing","author":"D. Fisman","year":"2009","unstructured":"Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.Y.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 7\u201322. Springer, Heidelberg (2009)"},{"key":"12_CR16","first-page":"17","volume":"2","author":"Y.V. Glebskii","year":"1969","unstructured":"Glebskii, Y.V., Kogan, D.I., Liogonkii, M.I., Talanov, V.A.: Range and degree of realizability of formulas in the restricted predicate calculus. Kibernetika\u00a02, 17\u201328 (1969)","journal-title":"Kibernetika"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-30494-4_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 306\u2013321. Springer, Heidelberg (2004)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-540-24730-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: How vacuous is vacuous? In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 451\u2013466. Springer, Heidelberg (2004)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11817949_3","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O.: Sanity checks in formal verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 37\u201351. Springer, Heidelberg (2006)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Li, W., Seshia, S.A.: A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: FMCAD 2008, pp. 1\u20139 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.29"},{"issue":"2","key":"12_CR21","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. STTT\u00a04(2), 224\u2013233 (2003)","journal-title":"STTT"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-02444-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T00:20:46Z","timestamp":1558052446000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02444-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319024431","9783319024448"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02444-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}