{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:10:16Z","timestamp":1742919016046,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642237010"},{"type":"electronic","value":"9783642237027"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23702-7_21","type":"book-chapter","created":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T17:31:31Z","timestamp":1315589491000},"page":"263-279","source":"Crossref","is-referenced-by-count":1,"title":["An Abstraction-Refinement Framework for Trigger Querying"],"prefix":"10.1007","author":[{"given":"Guy","family":"Avni","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The forSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 196\u2013211. Springer, Heidelberg (2002)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11513988_8","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2005","unstructured":"Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 67\u201381. Springer, Heidelberg (2005)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Temporal logic query checking. In: Proc. 16th LICS, pp. 409\u2013420. IEEE Computer Society, Los Alamitos (2001)","DOI":"10.1109\/LICS.2001.932516"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W. Chan","year":"2000","unstructured":"Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 450\u2013463. Springer, Heidelberg (2000)"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.: Quantitative languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 385\u2013400. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-87531-4_28"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-540-73210-5_15","volume-title":"Integrated Formal Methods","author":"M. Chechik","year":"2007","unstructured":"Chechik, M., Gheorghiu, M., Gurfinkel, A.: Finding state solutions to temporal logic queries. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 273\u2013292. Springer, Heidelberg (2007)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-45069-6_21","volume-title":"Computer Aided Verification","author":"M. Chechik","year":"2003","unstructured":"Chechik, M., Gurfinkel, A.: TLQSolver: A temporal logic query checker. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 210\u2013214. Springer, Heidelberg (2003)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","first-page":"76","volume-title":"Haifa Verification Conference","author":"H. Chockler","year":"2010","unstructured":"Chockler, H., Gurfinkel, A., Strichman, O.: Variants of LTL query checking. In: Raz, O. (ed.) HVC 2010. LNCS, vol.\u00a06504, pp. 76\u201392. Springer, Heidelberg (2010)"},{"issue":"5","key":"21_CR11","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"Journal of the ACM"},{"issue":"7","key":"21_CR12","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Gupta, A., Strichman, O.: Sat-based counterexample-guided abstraction refinement. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a023(7), 1113\u20131123 (2004)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"21_CR13","first-page":"238","volume-title":"Proc. 4th POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th POPL, pp. 238\u2013252. ACM, New York (1977)"},{"issue":"6","key":"21_CR14","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ic.2009.05.007","volume":"208","author":"L. Alfaro de","year":"2010","unstructured":"de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. Inf. Comput.\u00a0208(6), 666\u2013676 (2010)","journal-title":"Inf. Comput."},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-36577-X_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Glusman","year":"2003","unstructured":"Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 176\u2013191. Springer, Heidelberg (2003)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45657-0_11","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 137\u2013150. Springer, Heidelberg (2002)"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional must program analysis: unleashing the power of alternation. In: Proc. 37th POPL, pp. 43\u201356 (2010)","DOI":"10.1145\/1706299.1706307"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Lange, M., Leucker, M., Shoham, S.: Don\u2019t know in the \u03bc-calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 233\u2013249. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-30579-8_16"},{"issue":"10","key":"21_CR19","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1109\/TSE.2003.1237171","volume":"29","author":"A. Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Trans. Software Eng.\u00a029(10), 898\u2013914 (2003)","journal-title":"IEEE Trans. Software Eng."},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"K\u00fchne, U., Gro\u00dfe, D., Drechsler, R.: Property analysis and design understanding. In: DATE, pp. 1246\u20131249 (2009)","DOI":"10.1109\/DATE.2009.5090855"},{"key":"21_CR21","first-page":"146","volume-title":"Proc. 7th Int. Conf. on Formal Methods in Computer-Aided Design","author":"O. Kupferman","year":"2007","unstructured":"Kupferman, O., Lustig, Y.: What triggers a behavior? In: Proc. 7th Int. Conf. on Formal Methods in Computer-Aided Design, pp. 146\u2013153. IEEE Computer Society, Los Alamitos (2007)"},{"key":"21_CR22","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Press, Princeton (1994)"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, G.B.: A modal process logic. In: Proc. 3rd LICS (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Lo, D., Maoz, S.: Mining scenario-based triggers and effects. In: Proc. 23rd ASE, pp. 109\u2013118 (2008)","DOI":"10.1109\/ASE.2008.21"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-540-45220-1_38","volume-title":"Computer Science Logic","author":"M. Samer","year":"2003","unstructured":"Samer, M., Veith, H.: Validity of CTL queries revisited. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol.\u00a02803, pp. 470\u2013483. Springer, Heidelberg (2003)"},{"key":"21_CR26","volume-title":"A Practical Guide for SystemVerilog Assertions","author":"S. Vijayaraghavan","year":"2005","unstructured":"Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23702-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,15]],"date-time":"2019-06-15T03:03:06Z","timestamp":1560567786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23702-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237010","9783642237027"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23702-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}