{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T01:18:30Z","timestamp":1725671910500},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_20","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"195-209","source":"Crossref","is-referenced-by-count":2,"title":["Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study"],"prefix":"10.1007","author":[{"given":"Aditi","family":"Tagore","sequence":"first","affiliation":[]},{"given":"Diego","family":"Zaccai","sequence":"additional","affiliation":[]},{"given":"Bruce W.","family":"Weide","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_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)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-04211-9_4","volume-title":"Formal Foundations of Reuse and Domain Engineering","author":"J. Kirschenbaum","year":"2009","unstructured":"Kirschenbaum, J., Adcock, B., Bronish, D., Smith, H., Harton, H., Sitaraman, M., Weide, B.W.: Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping? In: Edwards, S.H., Kulczycki, G. (eds.) ICSR 2009. LNCS, vol.\u00a05791, pp. 31\u201340. Springer, Heidelberg (2009)"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/s00165-010-0154-3","volume":"23","author":"M. Sitaraman","year":"2011","unstructured":"Sitaraman, M., et al.: Building a push-button RESOLVE verifier: Progress and challenges. Formal Aspects of Computing\u00a023, 607\u2013626 (2011)","journal-title":"Formal Aspects of Computing"},{"key":"20_CR4","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 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"20_CR5","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":"20_CR6","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., Sitaraman, M., Harton, H.K., Adcock, B., Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J., Frazier, D.: 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":"20_CR7","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM\u00a050, 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"20_CR8","unstructured":"Heym, W.D.: Computer program verification: improvements for human reasoning. PhD thesis, The Ohio State University, Columbus, OH, USA (1995)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-44995-9_16","volume-title":"Software Reuse: Advances in Software Reusability","author":"M. Sitaraman","year":"2000","unstructured":"Sitaraman, M., Atkinson, S., Kulczycki, G., Weide, B.W., Long, T.J., Bucci, P., Heym, W.D., Pike, S.M., Hollingsworth, J.E.: Reasoning about Software-Component Behavior. In: Frakes, W.B. (ed.) ICSR 2000. LNCS, vol.\u00a01844, pp. 266\u2013283. Springer, Heidelberg (2000)"},{"key":"20_CR10","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. Marktoberdorf International Summer School 2008, lecture notes (2008)"},{"key":"20_CR11","unstructured":"Leino, K.R.M.: This is Boogie 2. Manuscript KRML 178 (2008), http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers.html"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15057-9_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., Monahan, R.: Dafny Meets the Verification Benchmarks Challenge. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 112\u2013126. Springer, Heidelberg (2010)"},{"key":"20_CR13","unstructured":"Nelson, C.G.: Techniques for program verification. PhD thesis, Stanford University, Stanford, CA, USA (1980)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"20_CR15","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM\u00a052, 365\u2013473 (2005)","journal-title":"J. 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-28891-3_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:03:14Z","timestamp":1606186994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}