{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:46:20Z","timestamp":1764402380617},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_29","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"258-262","source":"Crossref","is-referenced-by-count":58,"title":["Anzu: A Tool for Property Synthesis"],"prefix":"10.1007","author":[{"given":"Barbara","family":"Jobstmann","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Galler","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Weiglhofer","sequence":"additional","affiliation":[]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"ARM Ltd. AMBA Specification (Rev.\u00a02) (1999), available from \n                    \n                      www.arm.com"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: Proceedings of the Conference on Design, Automation and Test in Europe (to appear)","DOI":"10.1109\/DATE.2007.364456"},{"key":"29_CR3","doi-asserted-by":"publisher","first-page":"295","DOI":"10.2307\/1994916","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society\u00a0138, 295\u2013311 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"29_CR4","unstructured":"Church, A.: Logic, arithmetic and automata. In: Proceedings International Mathematical Congress (1962)"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722167_12","volume-title":"Computer Aided Verification","author":"J.H. Kukula","year":"2000","unstructured":"Kukula, J.H., Shiple, T.R.: Building circuits from relations. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 113\u2013123. Springer, Heidelberg (2000)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989. Proc. Symposium on Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"29_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society\u00a0141, 1\u201335 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"29_CR9","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)"},{"key":"29_CR10","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package. University of Colorado at Boulder \n                    \n                      ftp:\/\/vlsi.colorado.edu\/pub\/"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:30Z","timestamp":1619518110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_29","relation":{},"subject":[]}}