{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T08:02:24Z","timestamp":1750492944715},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678977"},{"type":"electronic","value":"9783540446187"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44618-4_41","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T14:38:51Z","timestamp":1188311931000},"page":"581-596","source":"Crossref","is-referenced-by-count":22,"title":["A Unifying Approach to Data-Independence"],"prefix":"10.1007","author":[{"given":"Ranko","family":"Lazi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Nowak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,12,21]]},"reference":[{"key":"41_CR1","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design, A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"41_CR2","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, R. Enders, T. Filkorn, and S. Jha. Exploiting Symmetry in Temporal Logic Model Checking. In [6], pages 77\u2013104, 1996. Kluwer.","DOI":"10.1007\/BF00625969"},{"key":"41_CR3","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction of Approximation of Fixed Points. In Proc. of POPL, pages 238\u2013252, 1977. ACM.","DOI":"10.1145\/512950.512973"},{"key":"41_CR5","unstructured":"S. J. Creese and A. W. Roscoe. Formal Verification of Arbitrary Network Topologies. In Proc. of PDPTA, Volume II, 1999. CSREA Press."},{"issue":"1\u20132","key":"41_CR6","volume":"9","year":"1996","unstructured":"E. A. Emerson (editor). Formal Methods in System Design 9(1\u20132) (Special Issue on Symmetry in Automatic Verification). Kluwer, 1996.","journal-title":"Formal Methods in System Design"},{"key":"41_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/3-540-60045-0_43","volume-title":"Proc. of CAV","author":"R. Hojati","year":"1995","unstructured":"R. Hojati and R. K. Brayton. Automatic Datapath Abstraction In Hardware Systems. In Proc. of CAV, volume 939 of LNCS, pages 98\u2013113, 1995. Springer Verlag."},{"key":"41_CR8","doi-asserted-by":"crossref","unstructured":"R. Hojati, D. L. Dill, and R. K. Brayton. Verifying linear temporal properties of data insensitive controllers using finite instantiations. In Proc. of CHDL, 1997.","DOI":"10.1007\/978-0-387-35064-6_5"},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"C. N. Ip and D. L. Dill. Better verification through symmetry. In [6], pages 41\u201375, 1996.","DOI":"10.1007\/BF00625968"},{"issue":"2","key":"41_CR10","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1006\/inco.1993.1069","volume":"107","author":"B. Jonsson","year":"1993","unstructured":"B. Jonsson and J. Parrow. Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs. Information and Computation, 107(2):272\u2013302, 1993.","journal-title":"Information and Computation"},{"key":"41_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0014552","volume-title":"Theoretical Aspects of Computer Software","author":"Y. Kinoshita","year":"1997","unstructured":"Y. Kinoshita, P. W. O\u2019Hearn, A. J. Power, and M. Takeyama. An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement. volume 1281 of LNCS, page 191, 1997."},{"key":"41_CR12","unstructured":"R. S. Lazi\u0107. A Semantic Study of Data Independence with Applications to Model Checking. D.Phil. thesis, Oxford University Computing Laboratory, 1999."},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"R. S. Lazi\u0107 and D. Nowak. A Unifying Approach to Data-independence. PRG Technical Report, Oxford University Computing Laboratory, 2000. Available at http:\/\/www.comlab.ox.ac.uk\/oucl\/publications\/tr\/index.html\u255aL .","DOI":"10.1007\/3-540-44618-4_41"},{"key":"41_CR14","unstructured":"R. S. Lazi\u0107 and A. W. Roscoe. Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays. In Proc. of INFINITY, Report TUM-I9825, Technical University of Munich, 1998. A fuller version is the Technical Report PRGTR-2-98, Oxford University Computing Laboratory."},{"key":"41_CR15","first-page":"319","volume":"I","author":"R. S. Lazi\u0107","year":"1999","unstructured":"R. S. Lazi\u0107 and A. W. Roscoe. Data Independence with Generalised Predicate Symbols. In Proc. of PDPTA, Volume I, pages 319\u2013325, 1999. CSREA Press.","journal-title":"Proc. of PDPTA"},{"key":"41_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CAV","author":"K. S. Namjoshi","year":"2000","unstructured":"K. S. Namjoshi and R. P. Kurshan. Syntactic Program Transformations for Automatic Abstraction. In Proc. of CAV, volume 1855 of LNCS, 2000. Springer Verlag."},{"key":"41_CR17","unstructured":"J. C. Reynolds. Types, Abstraction and Parametric Polymorphism. In Proc. of the IFIP 9th World Congress, pages 513\u2013523, 1983. Elsevier Science Publishers B. V. (Norht-Holland)."},{"key":"41_CR18","unstructured":"A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998."},{"key":"41_CR19","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe and P. J. Broadfoot. Proving security protocols with model checkers by data independence techniques. In J. of Comp. Sec., Special Issue CSFW11, page 147, 1999. IOS Press.","DOI":"10.3233\/JCS-1999-72-303"},{"key":"41_CR20","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on Infinite Objects. In [21], chapter 4, pages 133\u2013191. Elsevier Science Publishers B. V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"41_CR21","unstructured":"J. van Leeuwen. Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier Science Publishers B. V., 1990."},{"key":"41_CR22","unstructured":"M. Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In LICS, pages 332\u2013345, 1986. IEEE Computer Society Press."},{"key":"41_CR23","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing Interesting Properties of Programs in Propositional Temporal Logic. In Conference Record of POPL, pages 184\u2013193, 1986. ACM.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2000 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44618-4_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T17:09:44Z","timestamp":1556816984000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44618-4_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678977","9783540446187"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-44618-4_41","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}