{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:57:00Z","timestamp":1761929820438},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2016,4,6]],"date-time":"2016-04-06T00:00:00Z","timestamp":1459900800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1007\/s10009-016-0419-0","type":"journal-article","created":{"date-parts":[[2016,4,6]],"date-time":"2016-04-06T11:31:36Z","timestamp":1459942296000},"page":"697-716","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["AutoProof: auto-active functional verification of object-oriented programs"],"prefix":"10.1007","volume":"19","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[]},{"given":"Martin","family":"Nordio","sequence":"additional","affiliation":[]},{"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[]},{"given":"Julian","family":"Tschannen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,6]]},"reference":[{"key":"419_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., H\u00e4hnle, R., Hentschel, M., Herda, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The KeY platform for verification and analysis of Java programs. In: Verified Software: Theories, Tools, and Experiments (VSTTE 2014). Lecture Notes in Computer Science, no. 8471. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-12154-3_4"},{"key":"419_CR2","doi-asserted-by":"crossref","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 54(6), 81\u201391 (2011). http:\/\/specsharp.codeplex.com\/","DOI":"10.1145\/1953122.1953145"},{"key":"419_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: maintaining invariants over shared state. In: Mathematics of Program Construction. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"419_CR4","doi-asserted-by":"crossref","unstructured":"Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Information flow in object-oriented software. In: Logic-Based Program Synthesis and Transformation, 23rd International Symposium, LOPSTR. Lecture Notes in Computer Science, vol. 8901. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-14125-1_2"},{"key":"419_CR5","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H., (eds.) Verification of object-oriented software: the KeY Approach. In: LNCS, vol. 4334. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"key":"419_CR6","doi-asserted-by":"crossref","unstructured":"Bormer, T., et al.: The COST IC0701 verification competition 2011. In: FoVeOOS. LNCS, vol. 7421. Springer, Berlin (2012). http:\/\/foveoos2011.cost-ic0701.org\/verification-competition","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"419_CR7","doi-asserted-by":"crossref","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: FMCO, LNCS. Springer, Berlin. http:\/\/kindsoftware.com\/products\/opensource\/ESCJava2\/ (2006)","DOI":"10.1007\/11804192_16"},{"key":"419_CR8","doi-asserted-by":"crossref","unstructured":"Chimento, J.M., Ahrendt, W., Pace, G.J., Schneider, G.: StaRVOOrS: a tool for combined static and runtime verification of Java. In: Bartocci, E., Majumdar, R. (eds.) Runtime Verification\u20146th International Conference, RV 2015. Lecture Notes in Computer Science, vol. 9333. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-23820-3_21"},{"issue":"1","key":"419_CR9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods. Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods. Syst. Des."},{"key":"419_CR10","doi-asserted-by":"crossref","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: TPHOLs. LNCS, vol. 5674. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"419_CR11","unstructured":"Cok, D.: The OpenJML toolset. In: NASA Formal Methods, vol. 6617. (2011)"},{"issue":"6","key":"419_CR12","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1049\/iet-sen:20080011","volume":"2","author":"\u00c1 Darvas","year":"2008","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Faithful mapping of model classes to mathematical structures. IET Softw. 2(6), 477\u2013499 (2008)","journal-title":"IET Softw."},{"key":"419_CR13","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Upper Saddle River (1976)"},{"key":"419_CR14","unstructured":"EiffelBase2: A Fully Verified Container Library. https:\/\/github.com\/nadia-polikarpova\/eiffelbase2 (2015)"},{"key":"419_CR15","doi-asserted-by":"crossref","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transf. 17(6), 677\u2013694 (2015)","DOI":"10.1007\/s10009-014-0308-3"},{"key":"419_CR16","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.L.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: CAV. LNCS, vol. 4590. Springer, Berlin. http:\/\/krakatoa.lri.fr\/ (2007)","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"419_CR17","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3\u2014where programs meet provers. In: ESOP. LNCS, vol. 7792. Springer, Berlin. http:\/\/why3.lri.fr\/ (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"419_CR18","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A., Stump, A.: The 2nd verified software competition: experience report. In: COMPARE. CEUR Workshop Proceedings, vol. 873. CEUR-WS.org, 2012. https:\/\/sites.google.com\/site\/vstte2012\/compet (2012)"},{"key":"419_CR19","unstructured":"Furia, C.A.: Rotation of sequences: algorithms and proofs. http:\/\/arxiv.org\/abs\/1406.5453 (2014)"},{"key":"419_CR20","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Poskitt, C.M., Tschannen, J.: The AutoProof verifier: Usability by non-experts and on standard code. In: Dubois, C., Masci, P., Mery, D. (eds.) Proceedings of the 2nd Workshop on Formal Integrated Development Environment (F-IDE). Electronic Proceedings in Theoretical Computer Science, vol. 187, pp. 42\u201355. EPTCS, June 2015. Workshop co-located with FM (2015)","DOI":"10.4204\/EPTCS.187.4"},{"key":"419_CR21","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley, Boston (1995)"},{"key":"419_CR22","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition. http:\/\/verifythis2012.cost-ic0701.org (2012)"},{"key":"419_CR23","doi-asserted-by":"crossref","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition. http:\/\/etaps2015.verifythis.org\/ (2015)","DOI":"10.1007\/s10009-016-0438-x"},{"key":"419_CR24","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: APLAS. LNCS, vol. 6461. Springer, Berlin. http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/ (2010)","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"419_CR25","unstructured":"Jacobs, B., Smans, J., Piessens, F.: VeriFast: Imperative programs as proofs. In: VS-Tools Workshop at VSTTE (2010)"},{"key":"419_CR26","doi-asserted-by":"crossref","unstructured":"Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: FM. Springer, Berlin (2006)","DOI":"10.1007\/11813040_19"},{"key":"419_CR27","doi-asserted-by":"crossref","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: TGC. LNCS, vol. 4661. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75336-0_16"},{"key":"419_CR28","doi-asserted-by":"crossref","unstructured":"Klebanov, V., et al.: The 1st verified software competition: experience report. In: FM. LNCS, vol. 6664. Springer, Berlin. https:\/\/sites.google.com\/a\/vscomp.org\/main\/ (2011)","DOI":"10.1007\/978-3-642-21437-0_14"},{"issue":"1\u20133","key":"419_CR29","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"GT 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. 55(1\u20133), 185\u2013208 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"419_CR30","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"GT Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Form. Aspects Comput. 19(2), 159\u2013189 (2007)","journal-title":"Form. Aspects Comput."},{"key":"419_CR31","unstructured":"Leino, K.R.M.: This is boogie 2. Technical Report, Microsoft Research. http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=147643 (2008)"},{"key":"419_CR32","unstructured":"Dafny: An automatic program verifier for functional correctness. In: LPAR-16. LNCS, vol. 6355. Springer, Berlin. http:\/\/research.microsoft.com\/en-us\/projects\/dafny\/ (2010)"},{"key":"419_CR33","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop. http:\/\/fm.csl.sri.com\/UV10\/ (2010)"},{"key":"419_CR34","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: ECOOP 2004\u2014Object-Oriented Programming, 18th European Conference, Oslo, Norway, June 14\u201318, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3086. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"419_CR35","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: ECOOP. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"419_CR36","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17\u201319, 2002, pp. 246\u2013257 (2002)","DOI":"10.1145\/512529.512559"},{"key":"419_CR37","doi-asserted-by":"crossref","unstructured":"Logozzo, F.: Our experience with the CodeContracts static checker. In: 241 VSTTE. LNCS, vol. 7152. Springer, Berlin. http:\/\/msdn.microsoft.com\/en-us\/devlabs\/dd491992.aspx (2012)","DOI":"10.1007\/978-3-642-27705-4_19"},{"key":"419_CR38","unstructured":"The OpenJML Toolset. http:\/\/openjml.org\/ (2013)"},{"key":"419_CR39","doi-asserted-by":"crossref","unstructured":"Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201914, Edinburgh, United Kingdom, June 09\u201311, 2014, p. 46 (2014)","DOI":"10.1145\/2666356.2594325"},{"key":"419_CR40","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Furia, C.A., Meyer, B.: Specifying reusable components. In: VSTTE. LNCS, vol. 6217. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15057-9_9"},{"key":"419_CR41","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: FM LNCS. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-19249-9_26"},{"key":"419_CR42","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A., Meyer, B.: Flexible invariants through semantic collaboration. In: FM. LNCS, vol. 8442. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"419_CR43","unstructured":"SAVCBS workshop series. http:\/\/www.eecs.ucf.edu\/~leavens\/SAVCBS\/ (2010)"},{"key":"419_CR44","doi-asserted-by":"crossref","unstructured":"Summers, A.J., Drossopoulou, S., M\u00fcller, P.: The need for flexible object invariants. In: IWACO, pp. 1\u20139. ACM, New York (2009)","DOI":"10.1145\/1562154.1562160"},{"key":"419_CR45","doi-asserted-by":"crossref","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: SAS. LNCS, vol. 6887. Springer, Berlin. http:\/\/leon.epfl.ch\/ (2011)","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"419_CR46","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M.: AutoProof meets some verification challenges. Int. J. Softw. Tools Technol. Transf. 17(6), 745\u2013755 (2015)","DOI":"10.1007\/s10009-014-0300-y"},{"key":"419_CR47","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: SEFM. LNCS, vol. 7041. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"419_CR48","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Automatic verification of advanced object-oriented features: the AutoProof approach. In: Tools for Practical Software Verification. LNCS, vol. 7682. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-35746-6_5"},{"key":"419_CR49","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Program checking with less hassle. In: VSTTE 2013, vol. 8164. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54108-7_8"},{"key":"419_CR50","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C., et al. (eds.) Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of systems (TACAS). Lecture Notes in Computer Science, vol. 9035, pp. 566\u2013580. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"419_CR51","doi-asserted-by":"crossref","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: VSTTE. LNCS, no. 5295, pp. 84\u201398. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-87873-5_10"},{"key":"419_CR52","doi-asserted-by":"crossref","unstructured":"West, S., Nanz, S., Meyer, B.: Efficient and reasonable object-oriented concurrency. In Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201915). ACM, New York (2015)","DOI":"10.1145\/2786805.2786822"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0419-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0419-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0419-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0419-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,6]],"date-time":"2019-09-06T05:10:42Z","timestamp":1567746642000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0419-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,6]]},"references-count":52,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["419"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0419-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,6]]}}}