{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T10:10:02Z","timestamp":1746267002271,"version":"3.40.4"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319076010"},{"type":"electronic","value":"9783319076027"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07602-7_12","type":"book-chapter","created":{"date-parts":[[2014,6,12]],"date-time":"2014-06-12T11:29:08Z","timestamp":1402572548000},"page":"174-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Axioms and Abstract Predicates on Interfaces in Specifying\/Verifying OO Components"],"prefix":"10.1007","author":[{"given":"Ali","family":"Hong","sequence":"first","affiliation":[]},{"given":"Yijing","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,6,13]]},"reference":[{"key":"12_CR1","unstructured":"Aguirre, N., Maibaum, T.: A temporal logic approach to component-based system specification and reasoning. In: Proceedings of the 5th ICSE Workshop on Component-Based Software Engineering. Citeseer (2002)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"issue":"6","key":"12_CR3","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Experience 35(6), 583\u2013599 (2005)","journal-title":"Softw. Pract. Experience"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular OO verification with separation logic. In: POPL\u201908, pp. 87\u201399. ACM (2008)","DOI":"10.1145\/1328897.1328452"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"De Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC\/FSE\u201901, vol. 26, pp. 109\u2013120. ACM (2001)","DOI":"10.1145\/503271.503226"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for java. In: OOPSLA\u201908, pp. 213\u2013226. ACM (2008)","DOI":"10.1145\/1449955.1449782"},{"key":"12_CR7","volume-title":"Design Patterns, Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns, Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1994)"},{"issue":"12","key":"12_CR8","doi-asserted-by":"publisher","first-page":"1048","DOI":"10.1145\/359657.359666","volume":"21","author":"JV Guttag","year":"1978","unstructured":"Guttag, J.V., Horowitz, E., Musser, D.R.: Abstract data types and software validation. Commun. ACM 21(12), 1048\u20131064 (1978)","journal-title":"Commun. ACM"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Hong, A., Liu, Y., Qiu, Z.: Axioms and abstract predicates on interfaces in specifying\/verifying OO components. Technical report, School of Mathamatics, Peking University (2013). https:\/\/github.com\/zyqiu\/tr\/blob\/master\/OO-components-rep.pdf","DOI":"10.1007\/978-3-319-07602-7_12"},{"issue":"3","key":"12_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"12_CR11","first-page":"113","volume-title":"Foundations of Component-Based Systems, Chap. 6","author":"GT Leavens","year":"2000","unstructured":"Leavens, G.T., Dhara, K.K.: Concepts of behavioral subtyping and a sketch of their extension to component-based systems. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, Chap. 6, pp. 113\u2013135. Cambridge University Press, Cambridge (2000)"},{"key":"12_CR12","doi-asserted-by":"publisher","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. Formal Aspects Comput. 19, 159\u2013189 (2007)","journal-title":"Formal Aspects Comput."},{"key":"12_CR13","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping is equivalent to modular reasoning for object-oriented programs. Technical Report, Department of Computer Science, Iowa State University (2006)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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":"KRM 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 (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"issue":"6","key":"12_CR15","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Liu, Y., Hong, A., Qiu, Z.: Inheritance and modularity in specification and verification of OO programs. In: TASE\u201911, pp. 19\u201326. IEEE Computer Society (2011)","DOI":"10.1109\/TASE.2011.28"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-27269-1_6","volume-title":"Formal Aspects of Component Software","author":"L Yijing","year":"2012","unstructured":"Yijing, L., Zongyan, Q.: A separation logic for OO programs. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 88\u2013105. Springer, Heidelberg (2012)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL\u201908, pp. 75\u201386. ACM (2008)","DOI":"10.1145\/1328897.1328451"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/11804192_15","volume-title":"Formal Methods for Components and Objects","author":"A Poetzsch-Heffter","year":"2006","unstructured":"Poetzsch-Heffter, A., Sch\u00e4fer, J.: Modular specification of encapsulated object-oriented components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 313\u2013341. Springer, Heidelberg (2006)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-34281-3_13","volume-title":"Formal Methods and Software Engineering","author":"Q Zongyan","year":"2012","unstructured":"Zongyan, Q., Ali, H., Yijing, L.: Modular verification of OO programs with interfaces. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 151\u2013166. Springer, Heidelberg (2012)"},{"key":"12_CR21","unstructured":"Qiu, Z., Wang, S., Long, Q.: Sequential $${\\mu }$$Java: Formal foundations. Technical Report 2007\u201335, School of Mathamatics, Peking University (2007). http:\/\/www.mathinst.pku.edu.cn\/index.php?styleid=2"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Van Staden, S., Calcagno, C.: Reasoning about multiple related abstractions with multistar. In: OOPSLA\u201910, pp. 504\u2013519. ACM (2010)","DOI":"10.1145\/1932682.1869501"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07602-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:44:06Z","timestamp":1746265446000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-07602-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319076010","9783319076027"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07602-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"13 June 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}