{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:51Z","timestamp":1767929271224,"version":"3.49.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2011,7,10]],"date-time":"2011-07-10T00:00:00Z","timestamp":1310256000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-011-0207-9","type":"journal-article","created":{"date-parts":[[2011,7,9]],"date-time":"2011-07-09T09:44:36Z","timestamp":1310204676000},"page":"585-601","source":"Crossref","is-referenced-by-count":21,"title":["Synthesis of AMBA AHB from formal specification: a case study"],"prefix":"10.1007","volume":"15","author":[{"given":"Yashdeep","family":"Godhal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,7,10]]},"reference":[{"key":"207_CR1","unstructured":"ARM Ltd. Arm information center. http:\/\/infocenter.arm.com\/help\/index.jsp?topic=\/com.arm.doc.faqs\/588.html"},{"key":"207_CR2","unstructured":"ARM Ltd. Arm information center. http:\/\/infocenter.arm.com\/help\/index.jsp?topic=\/com.arm.doc.faqs\/ka3455.html"},{"key":"207_CR3","unstructured":"ARM Ltd. Arm information center. http:\/\/infocenter.arm.com\/help\/index.jsp?topic=\/com.arm.doc.faqs\/ka3462.html"},{"key":"207_CR4","unstructured":"ARM Ltd. Amba specification (rev. 2) http:\/\/www.arm.com\/products\/solutions\/AMBA_Spec.html (1999)"},{"key":"207_CR5","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: a system for sequential synthesis and verification, release 61225. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"207_CR6","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: DATE, pp. 1188\u20131193 (2007)","DOI":"10.1109\/DATE.2007.364456"},{"issue":"4","key":"207_CR7","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R. Bloem","year":"2007","unstructured":"Bloem R., Galler S., Jobstmann B., Piterman N., Pnueli A., Weiglhofer M.: Specify, compile, run: hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), 3\u201316 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"207_CR8","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J.R. Buchi","year":"1969","unstructured":"Buchi J.R., Landweber L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295\u2013311 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"207_CR9","unstructured":"Church, A.: Logic, arithmetic, and automata. In: Proceedings of International Congress Mathematical Union, Stockholm, pp. 23\u201335 (1963)"},{"key":"207_CR10","volume-title":"A practical introduction to PSL (series on integrated circuits and systems)","author":"C. Eisner","year":"2006","unstructured":"Eisner C., Fisman D.: A practical introduction to PSL (series on integrated circuits and systems). Springer, New York (2006)"},{"key":"207_CR11","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: CAV, pp. 258\u2013262 (2007)","DOI":"10.1007\/978-3-540-73368-3_29"},{"key":"207_CR12","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: VMCAI, pp. 364\u2013380 (2006)","DOI":"10.1007\/11609773_24"},{"key":"207_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"207_CR14","doi-asserted-by":"crossref","DOI":"10.1090\/cbms\/013","volume-title":"Automata on Infinite Objects and Church\u2019s Problem","author":"M.O. Rabin","year":"1972","unstructured":"Rabin M.O.: Automata on Infinite Objects and Church\u2019s Problem. American Mathematical Society, Boston (1972)"},{"key":"207_CR15","unstructured":"Somenzi, F.: Cudd: Cu decision diagram package. University of Colorado at Boulder. ftp:\/\/vlsi.colorado.edu\/pub\/"},{"key":"207_CR16","unstructured":"Williams, S.: Icarus verilog tool. ftp:\/\/ftp.icarus.com\/pub\/eda\/verilog\/v0.9"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0207-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0207-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0207-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T21:34:29Z","timestamp":1560375269000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0207-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,10]]},"references-count":16,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["207"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0207-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7,10]]}}}