{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:47:34Z","timestamp":1725763654600},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642538551"},{"type":"electronic","value":"9783642538568"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-53856-8_58","type":"book-chapter","created":{"date-parts":[[2013,12,10]],"date-time":"2013-12-10T08:26:45Z","timestamp":1386664005000},"page":"460-468","source":"Crossref","is-referenced-by-count":1,"title":["An Abstraction of Multi-port Memories with Arbitrary Addressable Units"],"prefix":"10.1007","author":[{"given":"Luk\u00e1\u0161","family":"Charv\u00e1t","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ale\u0161","family":"Smr\u010dka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"58_CR1","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers\u00a058 (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"58_CR2","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation\u00a098(2) (1992)","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"58_CR3","unstructured":"McCarthy, J.: Towards a\u00a0mathematical science of computation. In: IFIP Congress (1962)"},{"key":"58_CR4","doi-asserted-by":"crossref","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst.\u00a01(2) (1979)","DOI":"10.1145\/357073.357079"},{"key":"58_CR5","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A Decision Procedure for an\u00a0Extensional Theory of Arrays. In: Proc. of Logic in Computer Science. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"58_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2006","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"key":"58_CR7","unstructured":"German, S.M.: A Theory of Abstraction for Arrays. In: Proc. of FMCAD, Austin, TX (2011)"},{"key":"58_CR8","doi-asserted-by":"crossref","unstructured":"Koelbl, A., Burch, J., Pixley, C.: Memory Modeling in ESL-RTL Equivalence Checking. In: Proc. of DAC. IEEE Computer Society (2007)","DOI":"10.1109\/DAC.2007.375153"},{"key":"58_CR9","doi-asserted-by":"crossref","unstructured":"Koelbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver Technology for System-level to RTL Equivalence Checking. In: Proc. of DATE. IEEE Computer Society (2009)","DOI":"10.1109\/DATE.2009.5090657"},{"key":"58_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/3-540-63166-6_38","volume-title":"Computer Aided Verification","author":"M.N. Velev","year":"1997","unstructured":"Velev, M.N., Bryant, R.E., Jain, A.: Efficient Modeling of Memory Arrays in Symbolic Simulation. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 388\u2013399. Springer, Heidelberg (1997)"},{"key":"58_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-63875-X_40","volume-title":"Advances in Computing Science - ASIAN\u201997","author":"R.E. Bryant","year":"1997","unstructured":"Bryant, R.E., Velev, M.N.: Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. In: Shyamasundar, R.K., Ueda, K. (eds.) ASIAN 1997. LNCS, vol.\u00a01345, pp. 18\u201331. Springer, Heidelberg (1997)"},{"key":"58_CR12","unstructured":"Hunt Jr., W.A., Kaufmann, M.: A Formal Model of a Large Memory that Supports Efficient Execution. In: Proc. of FMCAD. IEEE Computer Society (2012)"},{"key":"58_CR13","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: Automatic Memory Reductions for RTL Model Verification. In: Proc. of ICCAD. ACM\/IEEE Computer Society (2006)","DOI":"10.1109\/ICCAD.2006.320121"},{"key":"58_CR14","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A., Ashar, P.: Verification of Embedded Memory Systems using Efficient Memory Modeling. In: Proc. of DATE. ACM\/IEEE Computer Society (2005)","DOI":"10.1109\/DATE.2005.325"},{"key":"58_CR15","unstructured":"McMillan, K.L.: Cadence SMV, http:\/\/www.kenmcmil.com\/smv.html"},{"key":"58_CR16","unstructured":"Smr\u010dka, A., Vojnar, T., Charv\u00e1t, L.: Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. In: Proc. of MTV (2012)"},{"key":"58_CR17","unstructured":"Codasip Studio for Rapid Processor Development, http:\/\/www.codasip.com"},{"key":"58_CR18","unstructured":"Codea2 Core IP in Codasip Studio, www.codasip.com\/products\/codea2\/"},{"key":"58_CR19","unstructured":"Naneshima, H., Iwanuma, K., Inoue, K.: GlueMinisat, appeared in SAT Competition 2011 (2011), http:\/\/sites.google.com\/a\/nabelab.org\/glueminisat\/"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Systems Theory - EUROCAST 2013"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-53856-8_58","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,4]],"date-time":"2019-08-04T15:05:12Z","timestamp":1564931112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-53856-8_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642538551","9783642538568"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-53856-8_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}