{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:08:06Z","timestamp":1762459686143},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319980461"},{"type":"electronic","value":"9783319980478"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_12","type":"book-chapter","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T21:05:49Z","timestamp":1540328749000},"page":"185-202","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modular Verification Scopes via Export Sets and Translucent Exports"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Matichuk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"12_CR1","unstructured":"Anindya Banerjee, David A. Naumann, and Stan Rosenberg. \u201cRegional logic for local reasoning about global invariants\u201d. In: Jan Vitek, editor ECOOP 2008, Object-Oriented Programming 22nd European Conference Springer, 2008."},{"key":"12_CR2","volume-title":"The Annotated C+ + Reference Manual","author":"Margaret A Ellis","year":"1990","unstructured":"Margaret A. Ellis and Bjarne Stroustrup. \u201cThe Annotated C+\u2009+ Reference Manual\u201d. In: Addison-Wesley Publishing Company, 1990."},{"key":"12_CR3","unstructured":"Jason Koenig and K. Rustan M. Leino. \u201cProgramming language features for refinement\u201d. In: In John Derrick, Eerke A. Boiten, and Steve Reeves, editors, Proceedings 17th International Workshop on Refinement, Refine@FM 2015 EPTCS, 2016."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"K. Rustan M. Leino. \u201cAccessible software verification with Dafny\u201d. In: IEEE Software IEEE, 2017.","DOI":"10.1109\/MS.2017.4121212"},{"key":"12_CR5","unstructured":"K. Rustan M. Leino. \u201cDafny: An automatic program verifier for functional correctness\u201d. In: Edmund M. Clarke and Andrei Voronkov editors, LPAR-16 Springer, 2010."},{"key":"12_CR6","unstructured":"Mark Lillibridge. \u201cTranslucent Sums: A Foundation for Higher-Order Module Systems\u201d. In: PhD thesis Carnegie Mellon University, 1997."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Peter M\u00fcller, Arnd Poetzsch-Heffter, and Gary T. Leavens \u201cModular invariants for layered object structures\u201d. In: Science of Computer Programming 2006.","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"12_CR8","unstructured":"Greg Nelson. \u201cSystems Programming with Modula-3\u201d. In: Series in Innovative Technology Prentice-Hall, Englewood Cliffs, NJ, 1991."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"D. L. Parnas. \u201cOn the criteria to be used in decomposing systems into modules\u201d. In: Communications of the ACM ACM, 1972.","DOI":"10.21236\/AD0773837"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Arnd Poetzsch-Heffter and Jan Sch\u00e4fer. \u201cModular specification of encapsulated object- oriented components\u201d. In: Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005 Springer, 2005.","DOI":"10.1007\/11804192_15"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Ina Schaefer and Arnd Poetzsch-Heffter. \u201cCompositional reasoning in model-based verification of adaptive embedded systems\u201d. In: Sixth IEEE International Conference on Software Engineering and Formal Methods (SEFM) IEEE Computer Society 2008.","DOI":"10.1109\/SEFM.2008.16"},{"key":"12_CR12","unstructured":"Ina Schaefer and Arnd Poetzsch-Heffter. \u201cUsing abstraction in modular verification of synchronous adaptive systems\u201d. In: Workshop on Trustworthy Software of OASICS Inter nationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, 2006."}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T13:15:01Z","timestamp":1572182101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_12","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}