{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:55:19Z","timestamp":1725900919514},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642380877"},{"type":"electronic","value":"9783642380884"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38088-4_18","type":"book-chapter","created":{"date-parts":[[2013,5,8]],"date-time":"2013-05-08T20:38:27Z","timestamp":1368045507000},"page":"261-275","source":"Crossref","is-referenced-by-count":1,"title":["Automatically Detecting Inconsistencies in Program Specifications"],"prefix":"10.1007","author":[{"given":"Aditi","family":"Tagore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruce W.","family":"Weide","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/190679.199221","volume":"19","author":"M. Sitaraman","year":"1994","unstructured":"Sitaraman, M., Weide, B.: Component-based software using RESOLVE. SIGSOFT Softw. Eng. Notes\u00a019, 21\u201363 (1994), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/190679.199221","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-87873-5_10","volume-title":"Verified Software: Theories, Tools, Experiments","author":"B.W. Weide","year":"2008","unstructured":"Weide, B.W., et al.: Incremental benchmarks for software verification tools and techniques. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 84\u201398. Springer, Heidelberg (2008)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-28891-3_20","volume-title":"NASA Formal Methods","author":"A. Tagore","year":"2012","unstructured":"Tagore, A., Zaccai, D., Weide, B.W.: Automatically proving thousands of verification conditions using an SMT solver: An empirical study. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 195\u2013209. Springer, Heidelberg (2012)"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Kemmerer, R.: Testing formal specifications to detect design errors. IEEE Transactions Software Engineering, 32\u201343 (1985)","DOI":"10.1109\/TSE.1985.231535"},{"key":"18_CR6","unstructured":"Kneuper, R.: Symbolic execution as a tool for validation of specifications. PhD thesis, University of Manchester (1989)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/11526841_7","volume-title":"FM 2005: Formal Methods","author":"F. Bouquet","year":"2005","unstructured":"Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: Symbolic animation of JML specifications. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 75\u201390. Springer, Heidelberg (2005)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/BFb0028775","volume-title":"Computer Aided Verification","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR: A toolset for specifying and analyzing software requirements. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 526\u2013531. Springer, Heidelberg (1998)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/ICSM.2010.5609573","volume-title":"Proceedings of the 2010 IEEE International Conference on Software Maintenance, ICSM 2010","author":"O. Ponsini","year":"2010","unstructured":"Ponsini, O., Collavizza, H., Fedele, C., Michel, C., Rueher, M.: Automatic verification of loop invariants. In: Proceedings of the 2010 IEEE International Conference on Software Maintenance, ICSM 2010, pp. 1\u20135. IEEE Computer Society, Washington, DC (2010)"},{"issue":"10","key":"18_CR11","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38088-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T19:34:43Z","timestamp":1557689683000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38088-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642380877","9783642380884"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38088-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}