{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,3]],"date-time":"2024-02-03T08:40:41Z","timestamp":1706949641859},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"8-9","license":[{"start":{"date-parts":[[2006,3,14]],"date-time":"2006-03-14T00:00:00Z","timestamp":1142294400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2006,4,7]]},"DOI":"10.1007\/s00236-006-0010-3","type":"journal-article","created":{"date-parts":[[2006,3,13]],"date-time":"2006-03-13T13:03:18Z","timestamp":1142254998000},"page":"639-671","source":"Crossref","is-referenced-by-count":2,"title":["Abstractions of data types"],"prefix":"10.1007","volume":"42","author":[{"given":"Ferucio Lauren\u0163iu","family":"\u0162iplea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,3,14]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Assmann, U., Weinhardt, M.: Interprocedural Heap Analysis for Parallelizing Imperative Programs, In: Giloi, W.K., J\u00e4hnichen, S., Shriver, B.D. (eds.) Programming Models for Massively Parallel Computers. IEEE Press, pp. 74\u201382 (1993)","DOI":"10.1109\/PMMP.1993.315553"},{"key":"10_CR2","unstructured":"Ball, Th., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs, Technical Report MSR-TR-2000-115, Microsoft Research (2000)"},{"key":"10_CR3","unstructured":"Bidoit, M., Boisseau A.: Algebraic Abstractions. In: 15th Workshop on Algebraic Development Techniques WADT'01, Lecture Notes in Computer Science 2267, 21\u201347 (2001)"},{"key":"10_CR4","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill D.: Symbolic Model Checking: 1020 States and Beyond, In: Proceedings of the 5th Symposium on Logic in Computer Science (1990)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Chase, D., Wegman, M., Zadeck F.: Analysis of Pointers and Structures, In: SIGPLAN Conference on Programming Languages, Design and Implementation, pp. 296\u2013310 (1990)","DOI":"10.1145\/93542.93585"},{"key":"10_CR6","unstructured":"Clarke, E.M., Grumberg, O., Peled D.A.: Model Checking, MIT Press (2000)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction, ACM Transactions on Programming Languages and Systems, pp. 1512\u20131542 (1994)","DOI":"10.1145\/186025.186051"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: 4th ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"10_CR9","unstructured":"Dams, D.: Abstract Interpretation and Partial Refinement for Model Checking, Ph.D. Thesis, Technische Universit\u00e4t Eindhoven (1996)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems, ACM Transactions on Programming Languages and Systems 19(2) (1997)","DOI":"10.1145\/244795.244800"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L., Park S.: Experience with Predicate Abstraction. In: Proceedings of the 11th International Conference on Computer Aided Verification CAV'99, Lecture Notes in Computer Science 1633, 160\u2013171 (1999)","DOI":"10.1007\/3-540-48683-6_16"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol Verification as a Hardware Design Aid. In: Proceedings of the IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, Springer-Verlag (1985)","DOI":"10.1007\/978-3-642-69962-7"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 2: Module Specifications and Constraints, Springer-Verlag (1990)","DOI":"10.1007\/978-3-642-61284-8"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Ehrig, H., Kreowski, H.-J.: Refinement and Implementation. In: Astesiano, E. et al. (eds.) Algebraic Foundations of Systems Specification, IFIP State-of-the-Art Report. Springer, pp. 201\u2013242 (1999)","DOI":"10.1007\/978-3-642-59851-7_7"},{"key":"10_CR16","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1111\/j.1467-8640.1988.tb00280.x","volume":"4","author":"M. Ginsberg","year":"1988","unstructured":"Ginsberg, M.: Multivalued Logics. A Uniform Approach to Inference in Artificial Intelligence, Computational Intelligence 4, 265\u2013316 (1988)","journal-title":"Computational Intelligence"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Proceedings of the 9th International Conference on Computer Aided Verification, Lecture Notes in Computer Science 1254, 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"10_CR18","unstructured":"The HOL System, Computer Laboratory, University of Cambridge, http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: A Practical Method for Verifying Event-driven Software. In: Proceedings of the 21st International Conference on Software Engineering ICSE'99, pp. 597\u2013607 (1999)","DOI":"10.1145\/302405.302710"},{"key":"10_CR20","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Primer and Reference Manual, Addison-Wesley (2003)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Pfeiffer, P., Reps, T.: Dependence Analysis for Pointer Variables. In: SIGPLAN Conference on Programming Languages, Design and Implementation, pp. 28\u201340 (1989)","DOI":"10.1145\/73141.74821"},{"key":"10_CR22","unstructured":"Jones, N.D., Muchnick, S.: Flow Analysis and Optimization of Lisp-like Structures. In: Muchnick, S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, Prentice-Hall, pp. 102\u2013131 (1981)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Muchnick, S.: A Flexible Approach to Interprocedural Data Flow Analysis and Programs with Recursive Data Structures. In: Symposium on Principles of Programing Languages, pp. 66\u201374 (1982)","DOI":"10.1145\/582153.582161"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press (1994)","DOI":"10.1515\/9781400864041"},{"issue":"8","key":"10_CR25","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A New Solution of the Dijkstra's Concurrent Problem, Communications of the ACM 17(8), 453\u2013455 (1974)","journal-title":"Communications of the ACM"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Larus, J., Hilfinger, P.: Detecting Conflicts Between Structure Accesses. In: SIGPLAN Conference on Programming Languages, Design and Implementation, pp. 21\u201334 (1988)","DOI":"10.1145\/53990.53993"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Loeckx, J., Ehrich, H.-D., Wolf, M.: Algebraic Specification of Abstract Data Types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 5, Clarendon Press, pp. 217\u2013316 (2000)","DOI":"10.1093\/oso\/9780198537816.003.0007"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal logic of Reactive and Concurrent Systems. Specification, Springer-Verlag (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Verification of Infinite State Systems by Compositional Model Checking, Research Report, Cadence Berkeley Labs (1999)","DOI":"10.1007\/3-540-48153-2_17"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Meinke, K., Tucker, J.V.: Universal Algebra, In: Abramsky, S., Gabbay, D., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science vol. 1, Oxford University Press, Oxford, pp. 189\u2013411 (1993)","DOI":"10.1093\/oso\/9780198537359.003.0003"},{"key":"10_CR31","unstructured":"Mitchell, J.: Foundations of Programming Languages, The MIT Press (1996)"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, Ch.: Principles of Program Analysis, Springer-Verlag (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Peled, D.A.: Software Reliability Methods, Springer-Verlag (2001)","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Plevyak, J., Chien, A., Karamcheti, V.: Analysis of Dynamic Structures for Efficient Parallel Execution. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D.: (eds.) Languages and Compilers for Parallel Computing Lecture Notes in Computer Science 768, Springer-Verlag, pp. 37\u201357 (1993)","DOI":"10.1007\/3-540-57659-2_3"},{"key":"10_CR35","unstructured":"The PVS Specification and Verification System, Computer Science Laboratory, SRI International, http:\/\/pvs.csl.sri.com"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Saidi, H.: Model Checking Guided Abstraction and Analysis, In: Proceedings of the 7th International Static Analysis Symposium (2000)","DOI":"10.1007\/978-3-540-45099-3_20"},{"issue":"1","key":"10_CR37","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, Th., Wilhelm, R.: Solving Shape-Analysis Problems in Languages with Destructive Updating, ACM Transaction on Programming Languages and Systems, 20(1), 1\u201350 (1998)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"issue":"3","key":"10_CR38","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, Th., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic, ACM Transaction on Programming Languages and Systems, 24(3), 217\u2013298 (2002)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"10_CR39","unstructured":"STeP: The Stanford Temporal Prover, http:\/\/www-step.stanford.edu"},{"issue":"1","key":"10_CR40","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/0890-5401(92)90076-R","volume":"101","author":"J. Stransky","year":"1992","unstructured":"Stransky, J.: A Lattice for Abstract Interpretation of Dynamic (Lisp-like) Structures, Information and Computation 101(1), 70\u2013102 (1992)","journal-title":"Information and Computation"},{"key":"10_CR41","unstructured":"Wang, E.Y.-B.: Analysis of Recursive Types in an Imperative Language, Ph.D. Thesis, University of California, Berkeley (1994)"},{"key":"10_CR42","doi-asserted-by":"crossref","unstructured":"Viser, W., Park, S., Penix, J.: Using Predicate Abstraction to Reduce Object-oriented Programs for Model Checking. In: Proceedings of the 3rd ACM Workshop on Formal Methods in Software Practice, Portland (Oregon), pp. 3\u201312 (2000)","DOI":"10.1145\/349360.351125"},{"key":"10_CR43","doi-asserted-by":"crossref","unstructured":"Visser, W., Park, S., Penix, J., Oh, P.: Abstracting Object-Oriented Programs for Model Checking, unpublished manuscript (2001)","DOI":"10.1145\/349360.351125"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0010-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-006-0010-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0010-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,3]],"date-time":"2024-02-03T08:23:46Z","timestamp":1706948626000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-006-0010-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,14]]},"references-count":43,"journal-issue":{"issue":"8-9","published-print":{"date-parts":[[2006,4,7]]}},"alternative-id":["10"],"URL":"https:\/\/doi.org\/10.1007\/s00236-006-0010-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,3,14]]}}}