{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:11:43Z","timestamp":1768003903097,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_53","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"566-580","source":"Crossref","is-referenced-by-count":60,"title":["AutoProof: Auto-Active Functional Verification of Object-Oriented Programs"],"prefix":"10.1007","author":[{"given":"Julian","family":"Tschannen","sequence":"first","affiliation":[]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Nordio","sequence":"additional","affiliation":[]},{"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"53_CR1","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M. Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM\u00a054(6), 81\u201391 (2011), \n                      \n                        http:\/\/specsharp.codeplex.com\/","journal-title":"Commun. ACM"},{"key":"53_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 54\u201384. Springer, Heidelberg (2004)"},{"key":"53_CR3","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"53_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-31762-0_2","volume-title":"Formal Verification of Object-Oriented Software","author":"T. Bormer","year":"2012","unstructured":"Bormer, T., et al.: The COST IC0701 verification competition 2011. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 3\u201321. Springer, Heidelberg (2012), \n                      \n                        http:\/\/foveoos2011.cost-ic0701.org\/verification-competition"},{"key":"53_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and eSC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006), \n                      \n                        http:\/\/kindsoftware.com\/products\/opensource\/ESCJava2\/"},{"key":"53_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009), \n                      \n                        http:\/\/vcc.codeplex.com\/"},{"key":"53_CR7","unstructured":"Cok, D.: The OpenJML toolset. In: NASA Formal Methods, vol. 6617 (2011)"},{"key":"53_CR8","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (1976)"},{"key":"53_CR9","unstructured":"EiffelBase2: A fully verified container library (2015), \n                      \n                        https:\/\/github.com\/nadia-polikarpova\/eiffelbase2"},{"key":"53_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007), \n                      \n                        http:\/\/krakatoa.lri.fr\/"},{"key":"53_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J.-C. Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2013 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 125\u2013128. Springer, Heidelberg (2013), \n                      \n                        http:\/\/why3.lri.fr\/"},{"key":"53_CR12","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A., Stump, A.: The 2nd verified software competition: Experience report. In: COMPARE. CEUR Workshop Proceedings, vol.\u00a0873, CEUR-WS.org (2012), \n                      \n                        https:\/\/sites.google.com\/site\/vstte2012\/compet"},{"key":"53_CR13","unstructured":"Furia, C.A.: Rotation of sequences: Algorithms and proofs (June 2014), \n                      \n                        http:\/\/arxiv.org\/abs\/1406.5453"},{"key":"53_CR14","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition (2012), \n                      \n                        http:\/\/verifythis2012.cost-ic0701.org"},{"key":"53_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B. Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 304\u2013311. Springer, Heidelberg (2010), \n                      \n                        http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/"},{"key":"53_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-75336-0_16","volume-title":"Trustworthy Global Computing","author":"J.R. Kiniry","year":"2007","unstructured":"Kiniry, J.R., Morkan, A.E., Cochran, D., Fairmichael, F., Chalin, P., Oostdijk, M., Hubbers, E.: The KOA remote voting system: A summary of work to date. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol.\u00a04661, pp. 244\u2013262. Springer, Heidelberg (2007)"},{"key":"53_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V. Klebanov","year":"2011","unstructured":"Klebanov, V., et al.: The 1st verified software competition: Experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 154\u2013168. Springer, Heidelberg (2011), \n                      \n                        https:\/\/sites.google.com\/a\/vscomp.org\/main\/"},{"issue":"1-3","key":"53_CR18","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program.\u00a055(1-3), 185\u2013208 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"53_CR19","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing\u00a019(2), 159\u2013189 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"53_CR20","unstructured":"Leino, K.R.M.: This is boogie 2. Technical report, Microsoft Research (June 2008), \n                      \n                        http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=147643"},{"key":"53_CR21","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), \n                      \n                        http:\/\/research.microsoft.com\/en-us\/projects\/dafny\/"},{"key":"53_CR22","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (November 2010), \n                      \n                        http:\/\/fm.csl.sri.com\/UV10\/"},{"key":"53_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.. M. Leino","year":"2004","unstructured":"Leino, K.R. M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013515. Springer, Heidelberg (2004)"},{"key":"53_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-27705-4_19","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F. Logozzo","year":"2012","unstructured":"Logozzo, F.: Our experience with the CodeContracts static checker. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 241\u2013242. Springer, Heidelberg (2012), \n                      \n                        http:\/\/msdn.microsoft.com\/en-us\/devlabs\/dd491992.aspx"},{"key":"53_CR25","unstructured":"The OpenJML toolset (2013), \n                      \n                        http:\/\/openjml.org\/"},{"key":"53_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-15057-9_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"N. Polikarpova","year":"2010","unstructured":"Polikarpova, N., Furia, C.A., Meyer, B.: Specifying reusable components. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 127\u2013141. Springer, Heidelberg (2010)"},{"key":"53_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-319-06410-9_35","volume-title":"FM 2014: Formal Methods","author":"N. Polikarpova","year":"2014","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A., Meyer, B.: Flexible invariants through semantic collaboration. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol.\u00a08442, pp. 514\u2013530. Springer, Heidelberg (2014)"},{"key":"53_CR28","unstructured":"SAVCBS workshop series (2010), \n                      \n                        http:\/\/www.eecs.ucf.edu\/~leavens\/SAVCBS\/"},{"key":"53_CR29","doi-asserted-by":"crossref","unstructured":"Summers, J., Drossopoulou, S., M\u00fcller, P.: The need for flexible object invariants. In: IWACO, pp. 1\u20139. ACM (2009)","DOI":"10.1145\/1562154.1562160"},{"key":"53_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Static Analysis","author":"P. Suter","year":"2011","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol.\u00a06887, pp. 298\u2013315. Springer, Heidelberg (2011), \n                      \n                        http:\/\/leon.epfl.ch\/"},{"key":"53_CR31","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M.: AutoProof meets some verification challenges. International Journal on Software Tools for Technology Transfer, 1\u201311 (February 2014)","DOI":"10.1007\/s10009-014-0300-y"},{"key":"53_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-642-24690-6_26","volume-title":"Software Engineering and Formal Methods","author":"J. Tschannen","year":"2011","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 382\u2013398. Springer, Heidelberg (2011)"},{"key":"53_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-35746-6_5","volume-title":"Tools for Practical Software Verification","author":"J. Tschannen","year":"2012","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Automatic verification of advanced object-oriented features: The AutoProof approach. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol.\u00a07682, pp. 133\u2013155. Springer, Heidelberg (2012)"},{"key":"53_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54108-7_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"J. Tschannen","year":"2014","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Program checking with less hassle. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol.\u00a08164, pp. 149\u2013169. Springer, Heidelberg (2014)"},{"key":"53_CR35","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: Auto-active functional verification of object-oriented programs (2015), \n                      \n                        http:\/\/arxiv.org\/abs\/1501.03063"},{"key":"53_CR36","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)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:26:17Z","timestamp":1559139977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}