{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T10:10:39Z","timestamp":1758708639461},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_32","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"479-494","source":"Crossref","is-referenced-by-count":3,"title":["Automatic Generation of Quality Specifications"],"prefix":"10.1007","author":[{"given":"Shaull","family":"Almagor","sequence":"first","affiliation":[]},{"given":"Guy","family":"Avni","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. TR (2013), \n                    \n                      http:\/\/leibniz.cs.huji.ac.il\/tr\/1300.pdf","DOI":"10.1007\/978-3-642-54862-8_37"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. ICALP 2013 (2013)","DOI":"10.1007\/978-3-642-39212-2_3"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proc. 25th STOC, pp. 592\u2013601 (1993)","DOI":"10.1145\/167088.167242"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. In: POPL, pp. 4\u201316 (2002)","DOI":"10.1145\/565816.503275"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Ammons, G., Mandelin, D., Bodk, R., Larus, J.R.: Debugging temporal specifications with concept analysis. In: Proc. PLDI, pp. 182\u2013195. Springer (2003)","DOI":"10.1145\/780822.781152"},{"issue":"2","key":"32_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput.\u00a075(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Avni, G., Kupferman, O.: Parameterized Weighted Containment. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol.\u00a07794, pp. 369\u2013384. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37075-5_24"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73368-3_30","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Cavada, R., Pill, I., Roveri, M., Tchaltsev, A.: RAT: A tool for the formal analysis of requirements. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: Proc. 26th LICS, pp. 43\u201352 (2011)","DOI":"10.1109\/LICS.2011.33"},{"key":"32_CR10","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":"32_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Proc. FMCAD, pp. 117\u2013124 (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 258\u2013262. Springer, Heidelberg (2007)"},{"key":"32_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"32_CR15","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":"32_CR16","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z.: Quantitative verification: models techniques and tools. In: ESEC\/SIGSOFT FSE, pp. 449\u2013458 (2007)","DOI":"10.1145\/1287624.1287688"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-69738-1_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Madhusudan","year":"2007","unstructured":"Madhusudan, P.: Learning algorithms and formal verification (Invited tutorial). In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 214\u2013214. Springer, Heidelberg (2007)"},{"issue":"2","key":"32_CR18","doi-asserted-by":"publisher","first-page":"1045","DOI":"10.1109\/TSMCB.2003.819485","volume":"34","author":"S. Moon","year":"2004","unstructured":"Moon, S., Lee, K., Lee, D.: Fuzzy branching temporal logic. IEEE Transactions on Systems, Man, and Cybernetics, Part B\u00a034(2), 1045\u20131055 (2004)","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics, Part B"},{"key":"32_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. TCS\u00a013, 45\u201360 (1981)","journal-title":"TCS"},{"key":"32_CR20","unstructured":"PROSYD. The Prosyd project on property-based system design, \n                    \n                      http:\/\/www.prosyd.org"},{"key":"32_CR21","unstructured":"Roveri, M.: Novel techniques for property assurance. TR PROSYD FP6-IST-507219 (2007)"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Proc. PLDI, pp. 281\u2013294 (2005)","DOI":"10.1145\/1064978.1065045"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:23:40Z","timestamp":1557930220000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}