{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:28:49Z","timestamp":1778300929698,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540581796","type":"print"},{"value":"9783540484691","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_55","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:16Z","timestamp":1330269916000},"page":"207-219","source":"Crossref","is-referenced-by-count":21,"title":["Verification of a distributed cache memory by using abstractions"],"prefix":"10.1007","author":[{"given":"Susanne","family":"Graf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Y. Afek, G. Brown, and M. Meritt. Lazy caching. ACM Transactions on Programming Languages and Systems, 15(1), 1993.","DOI":"10.1145\/151646.151651"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"P. and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977.","DOI":"10.1145\/512950.512973"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, D. Long. Model checking and abstraction. In POPL, 1991.","DOI":"10.1145\/143165.143235"},{"key":"17_CR4","unstructured":"J. Davis, R. Gerth, W. Jannsen, B. Jonsson, S. Katz, G. Lowe, A. Pnueli, and C. Rump. Verifying sequentially consistent memory. Preliminary report, 1993."},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and J. Y. Halpern. 'sometimes\u2019 and \u2018not never\u2019 revisited: On branching versus linear time. In POPL, 1983. also in Journal of ACM, 33:151\u2013178.","DOI":"10.1145\/4904.4999"},{"key":"17_CR6","unstructured":"S. Graf and C. Loiseaux. Program verification using compositional abstraction. In TAPSOFT 93, joint conference CAAP\/FASE. LNCS 668, Springer Verlag, April 1993."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In CAV, Heraklion Crete. LNCS 697, Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_7"},{"key":"17_CR8","unstructured":"B. Jonsson, A. Pnueli, and C. Rump. Proving refinement using transduction. Technical report, Weizmann Institute, 1993."},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Analysis of discrete event coordination. In REX Workshop on Stepwise Refinement of Distributed Systems, Mook. LNCS 430, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"17_CR10","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C-28","author":"L. Lamport","year":"1979","unstructured":"L. Lamport. How to make a multiprocessor that correctly executes multiprocess programs. IEEE Transactions on Computers, C-28:690\u2013691, 1979.","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR11","unstructured":"L. Lamport. The temporal logic of actions. Technical Report 79, DEC Systems Research Center, 1991."},{"key":"17_CR12","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. To appear in Formal Methods in System Design, also in CAV'92."},{"key":"17_CR13","volume-title":"Thesis","author":"C. Loiseaux","year":"1994","unstructured":"C. Loiseaux. V\u00e9rification symbolique de programmes r\u00e9actifs \u00e0 l'aide d'abstractions. Thesis, Verimag, Grenoble, January 1994."},{"key":"17_CR14","unstructured":"D. E. Long. Model checking, abstraction and compositional verification. Phd thesis, Carnegie Mellon University, July 1993."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models for Concurrent Systems. NATO, ASI Series F, Vol.13, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"17_CR16","volume-title":"Conference IFIP","author":"A. Pnueli","year":"1986","unstructured":"A. Pnueli. Specification and Development of reactive Systems. In Conference IFIP, Dublin. North-Holland, 1986."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"G. Shurek and O. Grumberg. The modular framework of computer-aided verification: motivation, solutions and evaluation criteria. In CAV, LNCS 531, 1990.","DOI":"10.1090\/dimacs\/003\/23"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_55.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:21:25Z","timestamp":1742595685000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}