{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:18:23Z","timestamp":1742912303075,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031331695"},{"type":"electronic","value":"9783031331701"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-33170-1_18","type":"book-chapter","created":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T12:55:27Z","timestamp":1685710527000},"page":"295-311","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From the Standards to Silicon: Formally Proved Memory Controllers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0292-3437","authenticated-orcid":false,"given":"Felipe Lisboa","family":"Malaquias","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5291-8567","authenticated-orcid":false,"given":"Mihail","family":"Asavoae","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2493-7864","authenticated-orcid":false,"given":"Florian","family":"Brandner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,3]]},"reference":[{"key":"18_CR1","unstructured":"Behrmann, G., et al.: Uppaal 4.0 (2006)"},{"issue":"1","key":"18_CR2","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1145\/291251.289440","volume":"34","author":"P Bjesse","year":"1998","unstructured":"Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: hardware design in Haskell. ACM SIGPLAN Notices 34(1), 174\u2013184 (1998)","journal-title":"ACM SIGPLAN Notices"},{"key":"18_CR3","unstructured":"Bourgeat, T., Clester, I., Erbsen, A., Gruetter, S., Wright, A., Chlipala, A.: A multipurpose formal RISC-V specification. arXiv preprint arXiv:2104.00762 (2021)"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Bourgeat, T., Pit-Claudel, C., Chlipala, A.: The essence of Bluespec: a core language for rule-based hardware design. In: 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 243\u2013257 (2020)","DOI":"10.1145\/3385412.3385965"},{"key":"18_CR5","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2022","unstructured":"Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2022)"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A., et al.: Kami: a platform for high-level parametric hardware specification and its modular verification (2017)","DOI":"10.1145\/3110268"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Datta, A., Singhal, V.: Formal verification of a public-domain DDR2 controller design. In: 21st International Conference on VLSI Design, pp. 475\u2013480. IEEE (2008)","DOI":"10.1109\/VLSI.2008.94"},{"key":"18_CR8","unstructured":"Dworkin, M.J., et al.: Advanced encryption standard (AES) (2001)"},{"issue":"5","key":"18_CR9","first-page":"1050","volume":"37","author":"M Hassan","year":"2017","unstructured":"Hassan, M., Patel, H.: MCXplore: automating the validation process of DRAM memory controller designs. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(5), 1050\u20131063 (2017)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"18_CR10","unstructured":"Joint Electron Device Engineering Council: DDR4 SDRAM standard (2021)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Kayed, M.O., Abdelsalam, M., Guindi, R.: A novel approach for SVA generation of DDR memory protocols based on TDML. In: 2014 15th International Microprocessor Test and Verification Workshop, pp. 61\u201366. IEEE (2014)","DOI":"10.1109\/MTV.2014.15"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Li, Y., Akesson, B., Lampka, K., Goossens, K.: Modeling and verification of dynamic command scheduling for real-time memory controllers. In: Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 1\u201312. IEEE (2016)","DOI":"10.1109\/RTAS.2016.7461341"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Lisboa Malaquias, F., Asavoae, M., Brandner, F.: A Coq framework for more trustworthy DRAM controllers. In: Proceedings of the 30th International Conference on Real-Time Networks and Systems, pp. 140\u2013150. ACM (2022)","DOI":"10.1145\/3534879.3534907"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3"},{"key":"18_CR15","unstructured":"Nikhil, R.: Bluespec system verilog: efficient, correct RTL from high level specifications. In: Proceedings 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, pp. 69\u201370. IEEE (2004)"},{"key":"18_CR16","first-page":"78","volume":"14","author":"D Park","year":"1981","unstructured":"Park, D.: A new equivalence notion for communicating systems. EATCS Bull. 14, 78\u201380 (1981)","journal-title":"EATCS Bull."},{"issue":"6","key":"18_CR17","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1007\/s00165-019-00497-w","volume":"31","author":"D Pous","year":"2019","unstructured":"Pous, D., Sangiorgi, D.: Bisimulation and coinduction enhancements: a historical perspective. Form. Asp. Comput. 31(6), 733\u2013749 (2019)","journal-title":"Form. Asp. Comput."},{"key":"18_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Steiner, L., Sudarshan, C., Jung, M., Stoffel, D., Wehn, N.: A framework for formal verification of DRAM controllers. arXiv preprint arXiv:2209.14021 (2022)","DOI":"10.1145\/3565053.3565059"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-030-27562-4_31","volume-title":"Embedded Computer Systems: Architectures, Modeling, and Simulation","author":"C Sudarshan","year":"2019","unstructured":"Sudarshan, C., Lappas, J., Weis, C., Mathew, D.M., Jung, M., Wehn, N.: A lean, low power, low latency DRAM memory controller for transprecision computing. In: Pnevmatikatos, D.N., Pelcat, M., Jung, M. (eds.) SAMOS 2019. LNCS, vol. 11733, pp. 429\u2013441. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-27562-4_31"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-33170-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,14]],"date-time":"2023-12-14T15:59:53Z","timestamp":1702569593000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-33170-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031331695","9783031331701"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-33170-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 June 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 May 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/nfm-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}