{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T01:58:58Z","timestamp":1725415138725},"reference-count":17,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1109\/memcod.2004.1459831","type":"proceedings-article","created":{"date-parts":[[2008,7,18]],"date-time":"2008-07-18T11:07:52Z","timestamp":1216379272000},"page":"119-128","source":"Crossref","is-referenced-by-count":1,"title":["The BUSpec platform for automated generation of verification aids for standard bus protocols"],"prefix":"10.1109","author":[{"family":"Bhaskar Pal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Ansuman Banerjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Pallab Dasgupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.P.","family":"Chakrabarti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"journal-title":"The BUSpec LRM Version 1 0","year":"0","key":"17"},{"journal-title":"Sugar Formal Property Language Reference Manual","year":"0","key":"15"},{"year":"0","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253709"},{"key":"14","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-40922-X_21","article-title":"A monitor-based formal specification of PCI","author":"shimizu","year":"2000","journal-title":"Proceedings of the Third International Conference of Formal Methods in Computer-Aided Design"},{"journal-title":"PCI Local Bus Specification Revision 2 2","year":"0","key":"11"},{"journal-title":"Property specification language Reference manual","year":"0","key":"12"},{"journal-title":"Berkeley Logic Interchange Format","year":"0","key":"3"},{"key":"2","article-title":"The forSpec temporal logic","author":"armoni","year":"0","journal-title":"Proc of TACAS'2001"},{"journal-title":"ARM AMBA Specification rev 2 0","year":"0","key":"1"},{"journal-title":"OpenVera LRM 2 0","year":"0","key":"10"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/ASIC.2000.880696"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/ASIC.1999.806467"},{"key":"4","article-title":"Verifying the performance of PCI local bus using symbolic techniques","author":"campos","year":"1995","journal-title":"IEEE Int Conf Computer Design"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/MWSCAS.2000.951664"},{"key":"8","article-title":"A specification methodology by a collection of compact properties as applied to the intel itanium processor bus protocol","author":"dill","year":"2001","journal-title":"Proc CHARME"}],"event":{"name":"Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04.","start":{"date-parts":[[2004,6,23]]},"location":"San Diego, CA, USA","end":{"date-parts":[[2004,6,25]]}},"container-title":["Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9882\/31414\/01459831.pdf?arnumber=1459831","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,18]],"date-time":"2017-06-18T06:01:45Z","timestamp":1497765705000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1459831\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"references-count":17,"URL":"https:\/\/doi.org\/10.1109\/memcod.2004.1459831","relation":{},"subject":[],"published":{"date-parts":[[2004]]}}}