{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:19:20Z","timestamp":1775053160080,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540878728","type":"print"},{"value":"9783540878735","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87873-5_10","type":"book-chapter","created":{"date-parts":[[2008,9,25]],"date-time":"2008-09-25T12:04:10Z","timestamp":1222344250000},"page":"84-98","source":"Crossref","is-referenced-by-count":24,"title":["Incremental Benchmarks for Software Verification Tools and Techniques"],"prefix":"10.1007","author":[{"given":"Bruce W.","family":"Weide","sequence":"first","affiliation":[]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[]},{"given":"Heather K.","family":"Harton","sequence":"additional","affiliation":[]},{"given":"Bruce","family":"Adcock","sequence":"additional","affiliation":[]},{"given":"Paolo","family":"Bucci","sequence":"additional","affiliation":[]},{"given":"Derek","family":"Bronish","sequence":"additional","affiliation":[]},{"given":"Wayne D.","family":"Heym","sequence":"additional","affiliation":[]},{"given":"Jason","family":"Kirschenbaum","sequence":"additional","affiliation":[]},{"given":"David","family":"Frazier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"ABZ call for papers on the POSIX pilot project in the grand challenge (viewed April 27, 2008), http:\/\/www.abz2008.org"},{"key":"10_CR2","unstructured":"Pacemaker formal methods challenge (viewed April 27, 2008), http:\/\/www.cas.mcmaster.ca\/sqrl\/pacemaker.htm"},{"key":"10_CR3","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: An electronic purse: specification, refinement, and proof. PRG Technical Monograph PRG-126 (2000), 231 pp. (viewed April 27, 2008), http:\/\/web2.comlab.ox.ac.uk\/oucl\/publications\/monos\/prg-126.html"},{"issue":"5","key":"10_CR4","first-page":"661","volume":"13","author":"J. Woodcock","year":"2007","unstructured":"Woodcock, J., Banach, R.: The verification grand challenge. Journal of Universal Computer Science\u00a013(5), 661\u2013668 (2007)","journal-title":"Journal of Universal Computer Science"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1109\/SEFM.2007.47","volume-title":"Fifth IEEE Intl. Conf. on Software Engineering and Formal Methods","author":"P.H. Schmitt","year":"2007","unstructured":"Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: Fifth IEEE Intl. Conf. on Software Engineering and Formal Methods, pp. 47\u201358. IEEE, Los Alamitos (2007)"},{"issue":"1","key":"10_CR6","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s00165-007-0057-0","volume":"20","author":"D. Haneberg","year":"2007","unstructured":"Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Formal Aspects of Computing\u00a020(1), 41\u201359 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"10_CR7","unstructured":"The POPLmark challenge (viewed April 27, 2008), http:\/\/alliance.seas.upenn.edu\/~plclub\/cgi-bin\/poplmark\/index.php?title=The_POPLmark_Challenge"},{"issue":"2","key":"10_CR8","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s00165-005-0079-4","volume":"18","author":"J.C. Bicarregui","year":"2006","unstructured":"Bicarregui, J.C., Hoare, C.A.R., Woodcock, J.C.P.: The verified software repository: a step towards the verifying compiler. Formal Aspects of Computing\u00a018(2), 143\u2013151 (2006)","journal-title":"Formal Aspects of Computing"},{"key":"10_CR9","unstructured":"Ancient Egyptian multiplication (viewed April 27, 2008), http:\/\/en.wikipedia.org\/wiki\/Ancient_Egyptian_multiplication"},{"key":"10_CR10","volume-title":"The Calculus of Computation","author":"A.R. Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007)"},{"key":"10_CR11","unstructured":"Bloch, J.: Extra, extra \u2013 read all about it: nearly all binary searches and mergesorts are broken (2006) (viewed 27 April 2008), http:\/\/googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/11590156_18","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"T. Zhang","year":"2005","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for queues with integer constraints. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 225\u2013237. Springer, Heidelberg (2005)"},{"issue":"4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf\u00a01(4), 271\u2013281 (1972)","journal-title":"Acta Inf"},{"issue":"3","key":"10_CR14","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/32.585503","volume":"23","author":"M. Sitaraman","year":"1997","unstructured":"Sitaraman, M., Weide, B.W., Ogden, W.F.: On the practical need for abstraction relations to verify abstract data type representations. IEEE Transactions on Software Engineering\u00a023(3), 157\u2013170 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Proc. 17th Annual IEEE Symp. on Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proc. 17th Annual IEEE Symp. on Logic in Computer Science, pp. 55\u201374. IEEE, Los Alamitos (2002)"},{"key":"10_CR16","unstructured":"Kulczycki, G.: Direct Reasoning. Dept. of Computer Science, Ph.D. thesis, ClemsonUniversity, Clemson, SC (2004)"},{"key":"10_CR17","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/1375581.1375624","volume-title":"ACM Conference on Programming Language Design and Implementation","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: ACM Conference on Programming Language Design and Implementation, pp. 349\u2013361. ACM Press, New York (2008)"},{"key":"10_CR18","unstructured":"Challenge problem: iterator specification (viewed April 27, 2008), http:\/\/www.eecs.ucf.edu\/~leavens\/SAVCBS\/2006\/challenge.shtml"},{"key":"10_CR19","unstructured":"Leavens, G., (ed.): SAVCBS 2006 Proceedings: Specification and Verification of Component-Based Systems (viewed April 27, 2008), http:\/\/www.eecs.ucf.edu\/~leavens\/SAVCBS\/2006\/SAVCBS06-proceedings.pdf"},{"key":"10_CR20","unstructured":"Booch, G.: Software components with Ada, Benjamin Cummings, Redwood City, CA (1987)"},{"issue":"8","key":"10_CR21","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1109\/32.310672","volume":"20","author":"B.W. Weide","year":"1994","unstructured":"Weide, B.W., Edwards, S.H., Harms, D.E., Lamb, D.A.: Design and specification of iterators using the swapping paradigm. IEEE Transactions on Software Engineering\u00a020(8), 631\u2013643 (1994)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"10_CR22","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/190679.190682","volume":"19","author":"S.H. Edwards","year":"1994","unstructured":"Edwards, S.H., Heym, W.D., Long, T.J., Sitaraman, M., Weide, B.W.: Specifying components in RESOLVE. Software Engineering Notes\u00a019(4), 29\u201339 (1994)","journal-title":"Software Engineering Notes"},{"issue":"4","key":"10_CR23","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/190679.190683","volume":"19","author":"P. Bucci","year":"1994","unstructured":"Bucci, P., Hollingsworth, J.E., Krone, J., Weide, B.W.: Implementing components in RESOLVE. Software Engineering Notes\u00a019(4), 40\u201352 (1994)","journal-title":"Software Engineering Notes"},{"key":"10_CR24","volume-title":"Encyc. of Computer Science and Engineering","author":"G. Kulczycki","year":"2008","unstructured":"Kulczycki, G., Sitaraman, M., Yasmin, N., Roche, K.: Formal specification. In: Encyc. of Computer Science and Engineering. John Wiley & Sons, Chichester (to appear, 2008)"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"10_CR26","unstructured":"Krone, J.: The Role of Verification in Software Reusability. Ph.D. dissertation, Dept. of Comp. and Inf. Science, Ohio State Univ., Columbus, OH (1988)"},{"key":"10_CR27","volume-title":"Encyc. of Computer Science and Engineering","author":"H. Harton","year":"2008","unstructured":"Harton, H., Krone, J., Sitaraman, M.: Formal program verification. In: Encyc. of Computer Science and Engineering. John Wiley & Sons, Chichester (to appear, 2008)"},{"key":"10_CR28","unstructured":"Heym, W.D.: Computer Program Verification: Improvements for Human Reasoning. Ph.D. dissertation, Dept. of Comp. and Inf. Sci., Ohio State Univ., Columbus, OH (1995)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., 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":"10_CR30","unstructured":"Zhang, J.: Program verification in the small. In: Proc. First Asian Working Conf. on Verified Software, UNU\/IIST Report #348, pp. 83\u201384 (2006)"},{"key":"10_CR31","unstructured":"JML BoundedStackInterface (viewed July 15, 2008), http:\/\/www.eecs.ucf.edu\/~leavens\/JML-release\/javadocs\/org\/jmlspecs\/samples\/stacks\/BoundedStackInterface.html"},{"key":"10_CR32","unstructured":"RESOLVE\/C++ Catalog, AT\/Stack\/Kernel.h (viewed July 15, 2008), http:\/\/www.cse.ohio-state.edu\/sce\/rcpp\/RESOLVE_Catalog-HTML\/AT\/Stack\/Kernel.html"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87873-5_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,17]],"date-time":"2021-09-17T03:51:15Z","timestamp":1631850675000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87873-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540878728","9783540878735"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87873-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}