乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:13:34Z","timestamp":1725491614241},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540744061"},{"type":"electronic","value":"9783540744078"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74407-8_33","type":"book-chapter","created":{"date-parts":[[2007,8,18]],"date-time":"2007-08-18T14:30:48Z","timestamp":1187447448000},"page":"492-506","source":"Crossref","is-referenced-by-count":10,"title":["Temporal Antecedent Failure: Refining Vacuity"],"prefix":"10.1007","author":[{"given":"Shoham","family":"Ben-David","sequence":"first","affiliation":[]},{"given":"Dana","family":"Fisman","sequence":"additional","affiliation":[]},{"given":"Sitvanit","family":"Ruah","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.: 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)"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: Design Automation Conference, pp. 596\u2013602 (1994)","DOI":"10.1145\/196244.196575"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 279\u2013290. Springer, Heidelberg (1997)"},{"issue":"2","key":"33_CR4","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 temporal model checking. Formal Methods in System Design\u00a018(2), 141\u2013163 (2001)","journal-title":"Formal Methods in System Design"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1998","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 184\u2013194. Springer, Heidelberg (1998)"},{"key":"33_CR6","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: Automata construction for regular expressions in model checking (IBM research report H-0229) (2004)"},{"key":"33_CR7","volume-title":"1st International Symposium on Leveraging Applications of Formal Methods","author":"S. Ben-David","year":"2004","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. In: Margaria, T., Steffen, B. (eds.) 1st International Symposium on Leveraging Applications of Formal Methods, Springer, Heidelberg (2004)"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/11678779_2","volume-title":"Hardware and Software, Verification and Testing","author":"S. Ben-David","year":"2006","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: The safety simple subset. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) Hardware and Software, Verification and Testing. LNCS, vol.\u00a03875, pp. 14\u201329. Springer, Heidelberg (2006)"},{"key":"33_CR9","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: Temporal antecedent failure: Refining vacuity (IBM research report H-0252) (2007)"},{"issue":"1","key":"33_CR10","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(86)90088-5","volume":"48","author":"G. Berry","year":"1986","unstructured":"Berry, G., Sethi, R.: From regular expressions to deterministic automata. Theoretical Computer Science\u00a048(1), 117\u2013126 (1986)","journal-title":"Theoretical Computer Science"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Boul\u2019e, M., Zilic, Z.: Efficient automata-based assertion-checker synthesis of psl properties. In: HLDVT 2006. Workshop on High LevelDesign, Validation, and Test (2006)","DOI":"10.1109\/HLDVT.2006.319966"},{"key":"33_CR12","unstructured":"Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science (2005)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2005)"},{"key":"33_CR14","unstructured":"Chechik, M., Gurfinkel, A., Gheorghiu, M.: Finding environmental guarantees. In: FASE 2007 (2007)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clarke","year":"1982","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"33_CR16","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (2000)"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45719-4_11","volume-title":"Algebraic Methodology and Software Technology","author":"Y. Dong","year":"2002","unstructured":"Dong, Y., saran Starosta, B., Ramakrishnan, C., Smolka, S.A.: Vacuity checking in the modal mu-claculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 147\u2013162. Springer, Heidelberg (2002)"},{"key":"33_CR18","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer (2006)"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"33_CR21","unstructured":"IBM\u2019s Model Checker RuleBase. http:\/\/www.haifa.il.ibm.com\/projects\/verification\/rb_homepage\/index.html"},{"key":"33_CR22","unstructured":"Annex E of IEEE Standard for SystemVerilog \u2014 Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800TM-2005"},{"key":"33_CR23","unstructured":"IEEE Standard for Property Specification Language (PSL). IEEE Std 1850TM-2005"},{"issue":"2","key":"33_CR24","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. STTT\u00a04(2), 224\u2013233 (2003)","journal-title":"STTT"},{"key":"33_CR25","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 Publishers, Dordrecht (1993)"},{"key":"33_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-540-27813-9_5","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2004","unstructured":"Namjoshi, K.S.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 57\u201369. Springer, Heidelberg (2004)"},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae, pp. 485\u2013499 (July 2002)","DOI":"10.1007\/3-540-45657-0_39"},{"key":"33_CR28","doi-asserted-by":"crossref","unstructured":"Quielle, J., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: 5th International Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"33_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/978-3-540-30494-4_23","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Samer","year":"2004","unstructured":"Samer, M., Veith, H.: Parametrized vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 322\u2013336. Springer, Heidelberg (2004)"},{"key":"33_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/11817963_20","volume-title":"Computer Aided Verification","author":"R. Tzoref","year":"2006","unstructured":"Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 190\u2013204. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2007 \u2013 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74407-8_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:25:07Z","timestamp":1619519107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74407-8_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744061","9783540744078"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74407-8_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}