{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:16:27Z","timestamp":1725574587714},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203636"},{"type":"electronic","value":"9783540397243"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39724-3_17","type":"book-chapter","created":{"date-parts":[[2011,1,8]],"date-time":"2011-01-08T02:15:55Z","timestamp":1294452955000},"page":"170-184","source":"Crossref","is-referenced-by-count":6,"title":["Reasoning about GSTE Assertion Graphs"],"prefix":"10.1007","author":[{"given":"Alan J.","family":"Hu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Casas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Aagaard, M., Jones, R.B., Seger, C.-J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: 35th Design Automation Conference, pp. 538\u2013541. ACM\/IEEE (1998)","DOI":"10.1145\/277044.277189"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-48153-2_7","volume-title":"Correct Hardware Design and Verification Methods","author":"N. Amla","year":"1999","unstructured":"Amla, N., Allen Emerson, E., Namjoshi, K.S.: Efficient decompositional modelchecking for regular timing diagrams. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 67\u201381. Springer, Heidelberg (1999)"},{"key":"17_CR3","volume-title":"International Workshop on High-Level Design, Validation, and Test","author":"B. Bentley","year":"2002","unstructured":"Bentley, B.: High level validation of next generation microprocessors. In: International Workshop on High-Level Design, Validation, and Test, IEEE, Los Alamitos (2002)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Computer Aided Verification","author":"P. Bjesse","year":"2001","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 454\u2013464. Springer, Heidelberg (2001)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Allen Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"17_CR6","volume-title":"Model Checking","author":"E.M. Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Hu, A.J., Casas, J., Yang, J.: Efficient generation of monitor circuits for GSTE assertion graphs. In: International Conference on Computer-Aided Design, IEEE\/ACM (2003) (to appear)","DOI":"10.1109\/ICCAD.2003.159685"},{"key":"17_CR8","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"17_CR9","first-page":"1","volume-title":"Symposium on Principles of Programming Languages","author":"Z. Manna","year":"1987","unstructured":"Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by \u2200-automata. In: Symposium on Principles of Programming Languages, pp. 1\u201312. ACM, New York (1987)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Nelson, K.L., Jain, A., Bryant, R.E.: Formal verification of a superscalar execution unit. In: 34th Design Automation Conference, pp. 161\u2013166. ACM\/IEEE (1997)","DOI":"10.1109\/DAC.1997.597137"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Oliveira, M.T., Hu, A.J.: High-level specification and automatic generation of IP interface monitors. In: 39th Design Automation Conference, pp. 129\u2013134. ACM\/IEEE (2002)","DOI":"10.1145\/513950.513952"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Pandey, M., Raimi, R., Beatty, D.L., Bryant, R.E.: Formal verification of PowerPC arrays using symbolic trajecory evaluation. In: 33rd Design Automation Conference, pp. 649\u2013654. ACM\/IEEE (1996)","DOI":"10.1145\/240518.240641"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/3-540-61440-0_140","volume-title":"Automata, Languages and Programming","author":"P. Raymond","year":"1996","unstructured":"Raymond, P.: Recognizing regular expressions by means of dataflow networks. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol.\u00a01099, pp. 336\u2013347. Springer, Heidelberg (1996)"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Seawright, A., Brewer, F.: High-level symbolic construction techniques for high performance sequential synthesis. In: 30th Design Automation Conference, pp. 424\u2013428. ACM\/IEEE (1993)","DOI":"10.1145\/157485.164961"},{"issue":"2","key":"17_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06(2), 147\u2013190 (1995)","journal-title":"Formal Methods in System Design"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"17_CR18","first-page":"332","volume-title":"Symposium on Logic in Computer Science","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science, pp. 332\u2013344. IEEE Computer Society, Los Alamitos (1986)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Yang, J., Goel, A.: GSTE through a case study. In: International Conference on Computer-Aided Design, pp. 534\u2013541. IEEE\/ACM (2002)","DOI":"10.1145\/774572.774651"},{"key":"17_CR20","first-page":"360","volume-title":"International Conference on Computer Design","author":"J. Yang","year":"2001","unstructured":"Yang, J., Seger, C.-J.H.: Introduction to generalized symbolic trajectory evaluation. In: International Conference on Computer Design, pp. 360\u2013365. IEEE, Los Alamitos (2001)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/3-540-36126-X_5","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Yang","year":"2002","unstructured":"Yang, J., Seger, C.-J.H.: Generalized symbolic trajectory evaluation \u2013 abstraction in action. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 70\u201387. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39724-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T18:03:30Z","timestamp":1559930610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}