{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,24]],"date-time":"2024-08-24T23:08:02Z","timestamp":1724540882142},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,10,25]],"date-time":"2013-10-25T00:00:00Z","timestamp":1382659200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10703-013-0200-x","type":"journal-article","created":{"date-parts":[[2013,10,24]],"date-time":"2013-10-24T09:21:40Z","timestamp":1382606500000},"page":"149-175","source":"Crossref","is-referenced-by-count":2,"title":["An abstraction-refinement framework for trigger querying"],"prefix":"10.1007","volume":"44","author":[{"given":"Guy","family":"Avni","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,10,25]]},"reference":[{"key":"200_CR1","series-title":"Lecture notes in computer science","first-page":"196","volume-title":"Proc 8th int conf on 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 MY, Zbar Y (2002) The ForSpec temporal logic: a new temporal property-specification logic. In: Proc 8th int conf on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 2280. Springer, Berlin, pp 196\u2013211"},{"key":"200_CR2","doi-asserted-by":"crossref","unstructured":"Avni G (2011) An abstraction-refinement framework for trigger querying. Msc Thesis","DOI":"10.1007\/978-3-642-23702-7_21"},{"key":"200_CR3","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/1217935.1217943","volume-title":"Proc EuroSys conf","author":"T Ball","year":"2006","unstructured":"Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey C, Ondrusek B, Rajamani SK, Ustuner\u00a0A (2006) Thorough static analysis of device drivers. In: Proc EuroSys conf, pp 73\u201385"},{"key":"200_CR4","first-page":"379","volume-title":"Proc 21st IEEE symp on logic in computer science","author":"T Ball","year":"2006","unstructured":"Ball T, Kupferman O (2006) An abstraction-refinement framework for multi-agent systems. In: Proc 21st IEEE symp on logic in computer science, pp 379\u2013388"},{"key":"200_CR5","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/11513988_8","volume-title":"Proc 17th int conf on computer aided verification","author":"T Ball","year":"2005","unstructured":"Ball T, Kupferman O, Yorsh G (2005) Abstraction for falsification. In: Proc 17th int conf on computer aided verification. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 67\u201381"},{"key":"200_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Proc 13th int conf on computer aided verification","author":"I Beer","year":"2001","unstructured":"Beer I, Ben-David S, Eisner C, Fisman D, Gringauze A, Rodeh Y (2001) The temporal logic sugar. In: Proc 13th int conf on computer aided verification. Lecture notes in computer science, vol 2102. Springer, Berlin, pp 363\u2013367"},{"key":"200_CR7","first-page":"409","volume-title":"Proc 16th IEEE symp on logic in computer science","author":"G Bruns","year":"2001","unstructured":"Bruns G, Godefroid P (2001) Temporal logic query checking. In: Proc 16th IEEE symp on logic in computer science. IEEE Comput Soc, Los Alamitos, pp 409\u2013420"},{"key":"200_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Proc 12th int conf on computer aided verification","author":"W Chan","year":"2000","unstructured":"Chan W (2000) Temporal-logic queries. In: Proc 12th int conf on computer aided verification. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 450\u2013463"},{"key":"200_CR9","first-page":"385","volume-title":"Proc 17th annual conf of the European association for computer science logic","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee K, Doyen L, Henzinger T (2008) Quantitative languages. In: Proc 17th annual conf of the European association for computer science logic, pp 385\u2013400"},{"key":"200_CR10","series-title":"Lecture notes in computer science","first-page":"273","volume-title":"Proc 6th int conf on integrated formal methods","author":"M Chechik","year":"2007","unstructured":"Chechik M, Gheorghiu M, Gurfinkel A (2007) Finding state solutions to temporal queries. In: Proc 6th int conf on integrated formal methods. Lecture notes in computer science, vol 4591. Springer, Berlin, pp\u00a0273\u2013292"},{"key":"200_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/978-3-540-45069-6_21","volume-title":"Proc 15th int conf on computer aided verification","author":"M Chechik","year":"2003","unstructured":"Chechik M, Gurfinkel A (2003) TLQSolver: a temporal logic query checker. In: Proc 15th int conf on computer aided verification. Lecture notes in computer science, vol 2725. Springer, Berlin, pp\u00a0210\u2013214"},{"key":"200_CR12","series-title":"Lecture notes in computer science","first-page":"76","volume-title":"Proc 6th int Haifa verification conference","author":"H Chockler","year":"2010","unstructured":"Chockler H, Gurfinkel A, Strichman O (2010) Variants of LTL query checking. In: Proc 6th int Haifa verification conference. Lecture notes in computer science, vol 6504. Springer, Berlin, pp 76\u201392"},{"issue":"5","key":"200_CR13","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"issue":"7","key":"200_CR14","doi-asserted-by":"crossref","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"EM Clarke","year":"2004","unstructured":"Clarke EM, Gupta A, Strichman O (2004) Sat-based counterexample-guided abstraction refinement. IEEE Trans Comput-Aided Des Integr Circuits Syst 23(7):1113\u20131123","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"200_CR15","first-page":"238","volume-title":"Proc 4th ACM symp on principles of programming languages","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proc 4th ACM symp on principles of programming languages. ACM, New York, pp 238\u2013252"},{"key":"200_CR16","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-0-387-35562-7_23","volume-title":"3rd IFIP int conf on formal methods for open object-based distributed systems","author":"W Damm","year":"1999","unstructured":"Damm W, Harel D (1999) LSCs: breathing life into message sequence charts. In: 3rd IFIP int conf on formal methods for open object-based distributed systems. Kluwer Academic, Dordrecht, pp 293\u2013312"},{"issue":"6","key":"200_CR17","doi-asserted-by":"crossref","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 (2010) Solving games via three-valued abstraction refinement. Inf Comput 208(6):666\u2013676","journal-title":"Inf Comput"},{"issue":"4","key":"200_CR18","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1093\/logcom\/8.4.457","volume":"8","author":"R Giacobazzi","year":"1998","unstructured":"Giacobazzi R (1998) Abductive analysis of modular logic programs. J Log Comput 8(4):457\u2013483","journal-title":"J Log Comput"},{"key":"200_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/3-540-36577-X_13","volume-title":"Proc 9th int conf on 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 MY (2003) Multiple-counterexample guided iterative abstraction refinement: an industrial evaluation. In: Proc 9th int conf on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 2619, pp 176\u2013191"},{"key":"200_CR20","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-45657-0_11","volume-title":"Proc 14th int conf on computer aided verification","author":"P Godefroid","year":"2002","unstructured":"Godefroid P, Jagadeesan R (2002) Automatic abstraction using generalized model checking. In: Proc 14th int conf on computer aided verification, vol 2404, pp 137\u2013150"},{"key":"200_CR21","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/1706299.1706307","volume-title":"Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages","author":"P Godefroid","year":"2010","unstructured":"Godefroid P, Nori AV, Rajamani SK, Tetali S (2010) Compositional may-must program analysis: unleashing the power of alternation. In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 43\u201356"},{"key":"200_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-540-30579-8_16","volume-title":"Proc 6th int conf on verification, model checking, and abstract interpretation","author":"O Grumberg","year":"2005","unstructured":"Grumberg O, Lange M, Leucker M, Shoham S (2005) Don\u2019t know in the \u03bc-calculus. In: Proc 6th int conf on verification, model checking, and abstract interpretation. Lecture notes in computer science, vol 3385. Springer, Berlin, pp 233\u2013249"},{"issue":"10","key":"200_CR23","doi-asserted-by":"crossref","first-page":"898","DOI":"10.1109\/TSE.2003.1237171","volume":"29","author":"A Gurfinkel","year":"2003","unstructured":"Gurfinkel A, Chechik M, Devereux B (2003) Temporal logic query checking: a tool for model exploration. IEEE Trans Softw Eng 29(10):898\u2013914","journal-title":"IEEE Trans Softw Eng"},{"key":"200_CR24","first-page":"1246","volume-title":"DATE","author":"U K\u00fchne","year":"2009","unstructured":"K\u00fchne U, Gro\u00dfe D, Drechsler R (2009) Property analysis and design understanding. In: DATE, pp 1246\u20131249"},{"key":"200_CR25","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 (2007) What triggers a behavior? In: Proc 7th int conf on formal methods in computer-aided design. IEEE Comput Soc, Los Alamitos, pp 146\u2013153"},{"key":"200_CR26","volume-title":"Computer aided verification of coordinating processes","author":"RP Kurshan","year":"1994","unstructured":"Kurshan RP (1994) Computer aided verification of coordinating processes. Princeton University Press, Princeton"},{"key":"200_CR27","first-page":"203","volume-title":"Proc 3rd IEEE symp on logic in computer science","author":"KG Larsen","year":"1988","unstructured":"Larsen KG, Thomsen GB (1988) A modal process logic. In: Proc 3rd IEEE symp on logic in computer science. IEEE Comput Soc, Los Alamitos, pp 203\u2013210"},{"key":"200_CR28","first-page":"109","volume-title":"Proc 23rd IEEE\/ACM international conference on automated software engineering","author":"D Lo","year":"2008","unstructured":"Lo D, Maoz S (2008) Mining scenario-based triggers and effects. In: Proc 23rd IEEE\/ACM international conference on automated software engineering, pp 109\u2013118"},{"key":"200_CR29","first-page":"46","volume-title":"Proc 18th IEEE symp on foundations of computer science","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proc 18th IEEE symp on foundations of computer science, pp 46\u201357"},{"key":"200_CR30","first-page":"470","volume-title":"Proc 12th annual conf of the European association for computer science logic","author":"M Samer","year":"2003","unstructured":"Samer M, Veith H (2003) Validity of CTL queries revisited. In: Proc 12th annual conf of the European association for computer science logic, vol 2803. Springer, Berlin, pp 470\u2013483"},{"key":"200_CR31","volume-title":"A practical guide for SystemVerilog assertions","author":"S Vijayaraghavan","year":"2005","unstructured":"Vijayaraghavan S, Ramanathan M (2005) A practical guide for SystemVerilog assertions. Springer, Berlin"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0200-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0200-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0200-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T15:34:02Z","timestamp":1688571242000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0200-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10,25]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["200"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0200-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,10,25]]}}}