{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T04:13:11Z","timestamp":1749615191488,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319452784"},{"type":"electronic","value":"9783319452791"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45279-1_12","type":"book-chapter","created":{"date-parts":[[2016,9,16]],"date-time":"2016-09-16T20:23:45Z","timestamp":1474057425000},"page":"171-186","source":"Crossref","is-referenced-by-count":0,"title":["Comparison Between Model Fields and Abstract Predicates"],"prefix":"10.1007","author":[{"given":"Ke","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,17]]},"reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"crossref","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. SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL 2005, pp. 247\u2013258. ACM (2005)","DOI":"10.1145\/1047659.1040326"},{"key":"12_CR3","unstructured":"Leino, K.R.: Toward reliable modular programs. Ph.D. thesis, California Institute of Technology (1995)"},{"key":"12_CR4","unstructured":"Bruns, D.: Formal semantics for the java modeling language. Diplomarbeit, Universit\u00e4t Karlsruhe, June 2009"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","author":"KRM Leino","year":"2006","unstructured":"Leino, K.R.M., M\u00fcller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 115\u2013130. Springer, Heidelberg (2006)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE CS (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL 2008, pp. 75\u201386. ACM (2008)","DOI":"10.1145\/1328438.1328451"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"12_CR9","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. CW Reports (2008)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998, pp. 48\u201364. ACM (1998)","DOI":"10.1145\/286942.286947"},{"key":"12_CR11","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual (2008)"},{"key":"12_CR12","unstructured":"Zhang, K., Qiu, Z.: Comparison between Model Fields and Abstract Predicates. Technical report, School of Math., Peking University (2016). https:\/\/github.com\/fm-pku\/mf-ap\/blob\/master\/mf-ap.pdf"},{"issue":"2","key":"12_CR13","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1002\/cpe.713","volume":"15","author":"P M\u00fcller","year":"2003","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency Comput. Pract. Exp. 15(2), 117\u2013154 (2003)","journal-title":"Concurrency Comput. Pract. Exp."},{"key":"12_CR14","unstructured":"Parkinson, M.: Class invariants: the end of the road. In: International Workshop on Aliasing, Confinement and Ownership, vol. 23 (2007)"},{"issue":"6","key":"12_CR15","doi-asserted-by":"crossref","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: research articles. Softw. Pract. Exp. 35(6), 583\u2013599 (2005)","journal-title":"Softw. Pract. Exp."},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., M\u00fcller, P.: Information hiding and visibility in interface specifications. In: ICSE 2007, pp. 385\u2013395. IEEE CS (2007)","DOI":"10.1109\/ICSE.2007.44"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Liu, Y., Hong, A., Qiu, Z.: Inheritance and modularity in specification and verification of OO programs. In: TASE 2011, pp. 19\u201326. IEEE CS (2011)","DOI":"10.1109\/TASE.2011.28"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/978-3-540-71289-3_26","volume-title":"Fundamental Approaches to Software Engineering","author":"\u00c1 Darvas","year":"2007","unstructured":"Darvas, \u00c1., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 336\u2013351. Springer, Heidelberg (2007)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Data groups: specifying the modification of extended state. In: OOPSLA 1998, pp. 144\u2013153. ACM (1998)","DOI":"10.1145\/286942.286953"},{"key":"12_CR21","unstructured":"Burgman, R.: Specifying multi-threaded Java programs (2010). http:\/\/referaat.cs.utwente.nl\/conference\/12\/paper"}],"container-title":["Lecture Notes in Computer Science","Programming Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45279-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T19:28:40Z","timestamp":1749583720000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45279-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319452784","9783319452791"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45279-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}