{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T19:44:40Z","timestamp":1749584680898,"version":"3.28.0"},"reference-count":19,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,8]]},"DOI":"10.1109\/tase.2011.28","type":"proceedings-article","created":{"date-parts":[[2011,10,13]],"date-time":"2011-10-13T16:58:19Z","timestamp":1318525099000},"page":"19-26","source":"Crossref","is-referenced-by-count":4,"title":["Inheritance and Modularity in Specification and Verification of OO Programs"],"prefix":"10.1109","author":[{"given":"Liu","family":"Yijing","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hong","family":"Ali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiu","family":"Zongyan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328452"},{"key":"ref12","article-title":"A weakest precondition semantics for Java","author":"yijing","year":"2010","journal-title":"Mathematics in School"},{"key":"ref13","article-title":"Sequential pJava: Formal foundations","author":"zongyan","year":"2007","journal-title":"Mathematics in School"},{"key":"ref14","article-title":"Behavioral subtyping is equivalent to modular reasoning for object-oriented programs","author":"leavens","year":"2006","journal-title":"Tech Rep"},{"key":"ref15","article-title":"Specification predicates: Linking abstract specification to implementation","author":"yijing","year":"2011","journal-title":"Mathematics in School"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0026-7"},{"key":"ref17","first-page":"2004","article-title":"Verification of object-oriented programs with invariants","volume":"3","author":"barnett","year":"2003","journal-title":"Journal of Object Technology"},{"journal-title":"ACSL ANSI C Specification Language (pre VI 2)","year":"2008","author":"baudin","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1002\/spe.649"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1127878.1127884","article-title":"Preliminary design of JML: A behavioral interface specification language for Java","volume":"31","author":"leavens","year":"2006","journal-title":"SIGSOFT Software Engineering Notes"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45651-1"},{"key":"ref5","article-title":"Toward reliable modular programs","author":"leino","year":"1995","journal-title":"Ph D Dissertation"},{"key":"ref8","doi-asserted-by":"crossref","DOI":"10.1145\/1040305.1040326","article-title":"Separation logic and abstraction","author":"parkinson","year":"2005","journal-title":"POPL'05"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286953"},{"key":"ref2","first-page":"49","article-title":"The Spec# programming system: An overview","author":"barnett","year":"2005","journal-title":"CASSIS 2004 ser LNCS 3362"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"journal-title":"Principles of Programming Languages (POPL)","article-title":"Separation logic, abstraction and inheritance","year":"2008","key":"ref9"}],"event":{"name":"2011 IEEE 5th International Symposium on Theoretical Aspects of Software Engineering (TASE)","start":{"date-parts":[[2011,8,29]]},"location":"Xi'an, China","end":{"date-parts":[[2011,8,31]]}},"container-title":["2011 Fifth International Conference on Theoretical Aspects of Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6041095\/6041600\/06042059.pdf?arnumber=6042059","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T03:55:55Z","timestamp":1497930955000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6042059\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8]]},"references-count":19,"URL":"https:\/\/doi.org\/10.1109\/tase.2011.28","relation":{},"subject":[],"published":{"date-parts":[[2011,8]]}}}