{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,3]],"date-time":"2023-08-03T19:15:14Z","timestamp":1691090114242},"reference-count":35,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"8","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. &amp; Syst."],"published-print":{"date-parts":[[2019,8,1]]},"DOI":"10.1587\/transinf.2018edp7254","type":"journal-article","created":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T22:10:53Z","timestamp":1564611053000},"page":"1498-1505","source":"Crossref","is-referenced-by-count":1,"title":["Consistency Checking between Java Equals and hashCode Methods Using Software Analysis Workbench"],"prefix":"10.1587","volume":"E102.D","author":[{"given":"Kozo","family":"OKANO","sequence":"first","affiliation":[{"name":"Shinshu University"}]},{"given":"Satoshi","family":"HARAUCHI","sequence":"additional","affiliation":[{"name":"Mitsubushi Electric Corporation"}]},{"given":"Toshifusa","family":"SEKIZAWA","sequence":"additional","affiliation":[{"name":"Nihon University"}]},{"given":"Shinpei","family":"OGATA","sequence":"additional","affiliation":[{"name":"Shinshu University"}]},{"given":"Shin","family":"NAKAJIMA","sequence":"additional","affiliation":[{"name":"National Institute of Informatics"}]}],"member":"532","reference":[{"key":"1","unstructured":"[1] N. Diakopoulos and S. Cass, \u201cInteractive: The Top Programming Languages 2016,\u201d http:\/\/spectrum.ieee.org\/static\/interactive-the-top-programming-languages-2016 (accessed March 20th 2017)."},{"key":"2","unstructured":"[2] Oracle, \u201cJava Platform, Standard Edition 7 API Specification,\u201d http:\/\/docs.oracle.com\/javase\/7\/docs\/api\/ (accessed March 20th 2017)."},{"key":"3","unstructured":"[3] Oracle, \u201cJava Platform Standard Ed. 8 AIP, class Object,\u201d https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/lang\/Object.html (accessed Oct. 20th 2017)."},{"key":"4","unstructured":"[4] K. Okano, H. Shimba, T. Ohta, H. Onoue, and S. Kusumoto, \u201cFormal verification technique for consistency checking between equals and hashCode methods in Java,\u201d International Journal on Informatics Society, vol.7, no.2, pp.77-87, 2015."},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] R. Dockins, A. Foltzer, J. Hendrix, B. Huffman, D. McNamee, and A. Tomb, \u201cConstructing semantic models of programs with the software analysis workbench,\u201d Proc. VSTTE 2016, 2016.","DOI":"10.1007\/978-3-319-48869-1_5"},{"key":"6","unstructured":"[6] Apache, \u201cApache PDFBox-A Java PDF Library,\u201d http:\/\/pdfbox.apache.org\/ (accessed March 20th 2017)."},{"key":"7","doi-asserted-by":"crossref","unstructured":"[7] D. Rayside, Z. Benjamin, R. Singh, J.P. Near, A. Milicevic, and D. Jackson, \u201cEquality and Hashing for (almost) Free: Generating Implementations from Abstraction Functions,\u201d Proc. 31st International Conference on Software Engineering, pp.342-352, 2009. 10.1109\/icse.2009.5070534","DOI":"10.1109\/ICSE.2009.5070534"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] N. Grech, J. Rathke, and B. Fischer, \u201cJEqualityGen: Generating Equality and Hashing Methods,\u201d Proc. ninth international conference on Generative programming and component engineering, pp.177-186, 2010. 10.1145\/1868294.1868320","DOI":"10.1145\/1868294.1868320"},{"key":"9","doi-asserted-by":"crossref","unstructured":"[9] T. Jensen, F. Kirchner, and D. Pichardie, \u201cSecure the clones: Static enforcement of policies for secure object copying,\u201d Proc. 20th European conference on Programming languages and systems, pp.317-337, 2010. 10.1007\/978-3-642-19718-5_17","DOI":"10.1007\/978-3-642-19718-5_17"},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] C.R. Rupakheti and D. Hou, \u201cAn Empirical Study of the Design and Implementation of Object Equality in Java,\u201d Proc. 2008 conference of the center for advanced studies on collaborative research: meeting of minds, pp.111-125, 2008. 10.1145\/1463788.1463800","DOI":"10.1145\/1463788.1463800"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] C.R. Rupakheti and D. Hou, \u201cAn Abstraction-Oriented, Path-Based Approach for Analyzing Object Equality in Java,\u201d Proc. 17th Working Conference on Reverse Engineering, pp.205-214, 2010. 10.1109\/wcre.2010.30","DOI":"10.1109\/WCRE.2010.30"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] C.R. Rupakheti and D. Hou, \u201cFinding Errors from Reverse-Engineered Equality Models using a Constraint Solver,\u201d Proc. 28th IEEE International Conference on Software Maintenance, pp.77-86, 2012. 10.1109\/icsm.2012.6405256","DOI":"10.1109\/ICSM.2012.6405256"},{"key":"13","unstructured":"[13] D. Jackson, Software Abstractions, Revised Edition Logic, Language, and Analysis, MIT Press, 2011."},{"key":"14","unstructured":"[14] C. Barrett, A. Stump, and C. Tinelli, \u201cThe SMT-LIB Standard Version 2.0,\u201d 2010."},{"key":"15","doi-asserted-by":"crossref","unstructured":"[15] K. Okano, S. Harauchi, T. Sekizawa, S. Ogata, and S. Nakajima, \u201cEquivalence checking of Java methods: Toward ensuring IoT dependability,\u201d Proc. 26th International Conference on Computer Communications and Networks, ICCCN 2017, pp.1-6, Aug. 2017.","DOI":"10.1109\/ICCCN.2017.8038505"},{"key":"16","unstructured":"[16] C.B. Lourenco, S.-M. Lamraoui, S. Nakajima, and J.S. Pinto, \u201cStudying verification conditions for imperative programs,\u201d Proc. 15th International Workshop on Automated Verification of Critical Systems, AVoCS&apos;15, 2015."},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] S.-M. Lamraoui and S. Nakajima, \u201cA Formula-based Approach for Automatic Fault Localization of Multi-fault Programs,\u201d Journal of Information Processing, vol.24, no.1, pp.88-98, 2016. 10.2197\/ipsjjip.24.88","DOI":"10.2197\/ipsjjip.24.88"},{"key":"18","doi-asserted-by":"publisher","unstructured":"[18] J.A. Darringer, W.H. Joyner, Jr., C.L. Berman, and L. Trevillyan, \u201cLogic synthesis through local transformations,\u201d IBM Journal of Research and Development, vol.25, no.4, pp.272-280, 1981. 10.1147\/rd.254.0272","DOI":"10.1147\/rd.254.0272"},{"key":"19","doi-asserted-by":"publisher","unstructured":"[19] R. Brayton and A. Mishchenko, \u201cABC: An Academic Industrial-Strength Verification Tool,\u201d LNCS, vol.6174, pp.24-40, 2010. 10.1007\/978-3-642-14295-6_5","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"20","doi-asserted-by":"publisher","unstructured":"[20] A. Kuehlmann, V. Paruthi, F. Krohm, and M.K. Ganai, \u201cRobust boolean reasoning for equivalence checking and functional property verification,\u201d IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol.21, no.12, pp.1377-1394, 2002. 10.1109\/tcad.2002.804386","DOI":"10.1109\/TCAD.2002.804386"},{"key":"21","doi-asserted-by":"publisher","unstructured":"[21] L. de Moura and N. Bj\u00f8rner, \u201cZ3: An efficient SMT solver,\u201d Proc. TACAS 2008, LNCS, vol.4963, pp.337-340, 2008. 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"22","doi-asserted-by":"publisher","unstructured":"[22] B. Dutertre, \u201cYices 2.2,\u201d Proc. CAV2014, LNCS, vol.8559, pp.737-744, 2014. 10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] C. Barrett, C.L. Conway, M. Deters, L. Hadarean, D. Jovanovi\u0107, T. King, A. Reynolds, and C. Tinelli, \u201cCVC4,\u201d Proc. 23rd international conference on Computer aided verification (CAV&apos;11), pp.171-177, 2011. 10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"24","doi-asserted-by":"crossref","unstructured":"[24] A. Cimatti, A. Griggio, B.J. Schaafsma, and R. Sebastiani, \u201cThe MathSAT5 SMT Solver,\u201d Proc. TACAS 2013, LNCS, vol.7795, pp.93-107, 2013. 10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"25","unstructured":"[25] A. Biere, M. Heule, H. Van Maaren, and T. Walsh, Handbook of Satisfiability, IOS Press, 2009."},{"key":"26","doi-asserted-by":"crossref","unstructured":"[26] L. Burdy, Y. Cheon, D.R. Cok, M.D. Ernst, J.R. Kiniry, G.T.Leavens, K.R.M. Leino, and E. Poll, \u201cAn overview of JML tools and applications,\u201d International Journal on Software Tools for Technology Transfer, pp.212-232, 2005.","DOI":"10.1007\/s10009-004-0167-4"},{"key":"27","unstructured":"[27] B. Meyer, Object-Oriented Software Construction, 2nd edition, Prentice Hall, 1997."},{"key":"28","doi-asserted-by":"crossref","unstructured":"[28] P. Chalin, J.R. Kiniry, G.T. Leavens, and E. Poll, \u201cBeyond Assertions: Advanced Specification and Verification with JML and ESC\/Java2,\u201d Proc. 4th International Symposium on Formal Methods for Components and Objects FMCO 2005, LNCS, vol.4111, pp.342-363, 2006. 10.1007\/11804192_16","DOI":"10.1007\/11804192_16"},{"key":"29","doi-asserted-by":"crossref","unstructured":"[29] J. S\u00e1nchez and G.T. Leavens, \u201cStatic verification of ptolemyrely programs using openJML,\u201d Proc. 13th workshop on Foundations of aspect-oriented languages, pp.13-18, 2014. 10.1145\/2588548.2588550","DOI":"10.1145\/2588548.2588550"},{"key":"30","doi-asserted-by":"publisher","unstructured":"[30] D. Detlefs, G. Nelson, and J.B. Saxe, \u201cSimplify: A Theorem Prover for Program Checking,\u201d Journal of the ACM, vol.52, no.3, pp.365-473, 2005. 10.1145\/1066100.1066102","DOI":"10.1145\/1066100.1066102"},{"key":"31","doi-asserted-by":"crossref","unstructured":"[31] M. Barnett, B.-Y.E. Chang, R. DeLine, B. Jacobs, and K.R.M. Leino, \u201cBoogie: A modular reusable verifier for object-oriented programs,\u201d Proc. 4th International Symposium on Formal Methods for Components and Objects FMCO 2005, LNCS, vol.4111, pp.364-387, 2006. 10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"32","doi-asserted-by":"publisher","unstructured":"[32] B. Dutertre and L. de Moura, \u201cA Fast Linear-Arithmetic Solver for DPLL(<i>T<\/i>),\u201d Proc. 18th Conference on Computer Aided Verification (CAV 2006), LNCS, vol.4144, pp.81-94, 2006. 10.1007\/11817963_11","DOI":"10.1007\/11817963_11"},{"key":"33","doi-asserted-by":"crossref","unstructured":"[33] K.L. McMillan, \u201cInterpolation and SAT-Based Model Checking,\u201d Proc. 15th Conference on Computer Aided Verification (CAV 2003), LNCS, vol.2725, pp.1-13, 2003. 10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"34","doi-asserted-by":"crossref","unstructured":"[34] A. Gurfinkel, T. Kahsai, A. Komuravelli, and J.A. Navas, \u201cThe SeaHorn Verification Framework,\u201d CAV 2015, LNCS, vol.9206, pp.343-361, 2015. 10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"35","doi-asserted-by":"crossref","unstructured":"[35] W. Ahrendt, B. Beckert, R. Bubel, R. H\u00e4hnle, P. Schmitt, and M. Ulbrich, Ed., Deductive Software Verification-The KeY Book-From Theory to Practice, Springer, 2016.","DOI":"10.1007\/978-3-319-49812-6"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E102.D\/8\/E102.D_2018EDP7254\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,3]],"date-time":"2019-08-03T03:29:53Z","timestamp":1564802993000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E102.D\/8\/E102.D_2018EDP7254\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,1]]},"references-count":35,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2019]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2018edp7254","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,8,1]]}}}