{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:48:03Z","timestamp":1725551283063},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_16","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:28Z","timestamp":1269882808000},"page":"202-218","source":"Crossref","is-referenced-by-count":1,"title":["Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving"],"prefix":"10.1007","author":[{"given":"Mark D.","family":"Aagaard","sequence":"first","affiliation":[]},{"given":"Thomas F.","family":"Melham","sequence":"additional","affiliation":[]},{"given":"John W.","family":"O\u2019Leary","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J.H. Seger. Formal verification using parametric representations of Boolean constraints. In ACM\/IEEE Design Automation Conference, July 1999.","DOI":"10.1145\/309847.309968"},{"key":"16_CR2","series-title":"Technical Report DAIMI IR-92","volume-title":"Automating a model checker for recursive modal assertions in HOL","author":"S. Agerholm","year":"1990","unstructured":"S. Agerholm and H. Skj\u00f8dt. Automating a model checker for recursive modal assertions in HOL. Technical Report DAIMI IR-92, Computer Science Department, Aarhus University, 1990."},{"key":"16_CR3","unstructured":"A. Cheng and K. Larsen, editors. Program and Abstracts of the BRICS Autumn School on the Verification, Aug. 1996. BRICS Notes Series NS-96-2."},{"key":"16_CR4","first-page":"310","volume-title":"HOL User\u2019s Group Workshop","author":"C. T. Chou","year":"1994","unstructured":"C. T. Chou. Predicates, temporal logic, and simulations. In C. J. H. Seger and J. J. Joyce, editors, HOL User\u2019s Group Workshop, pages 310\u2013323. Springer Verlag; New York, Aug. 1994."},{"key":"16_CR5","volume-title":"Workshop on Computer-Aided Verification","author":"C.T. Chou","year":"1999","unstructured":"C.T. Chou. The mathematical foundation of symbolic trajectory evaluation. In Workshop on Computer-Aided Verification. Springer Verlag; New York, 1999. To appear."},{"volume-title":"Formal Methods in Computer-Aided Design","year":"1998","key":"16_CR6","unstructured":"G. C. Gopalakrishnan and P. J. Windley, editors. Formal Methods in Computer-Aided Design. Springer Verlag; New York, Nov. 1998."},{"volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","key":"16_CR7","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York, 1993."},{"key":"16_CR8","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-63475-4_1","volume-title":"Formal Hardware Verification","author":"S. Hazelhurst","year":"1997","unstructured":"S. Hazelhurst and C.-J. H. Seger. Symbolic trajectory evaluation. In T. Kropf, editor, Formal Hardware Verification, chapter 1, pages 3\u201378. Springer Verlag; New York, 1997."},{"volume-title":"Computer Aided Verification","year":"1998","key":"16_CR9","unstructured":"A. J. Hu and M. Y. Vardi, editors. Computer Aided Verification. Springer Verlag; New York, July 1998."},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"J. Joyce and C.-J. Seger. Linking BDD based symbolic evaluation to interactive theorem proving. In ACM\/IEEE Design Automation Conference, June 1993.","DOI":"10.1145\/157485.164981"},{"volume-title":"Theorem Proving in Higher Order Logics","year":"1998","key":"16_CR11","unstructured":"M. Newey and J. Grundy, editors. Theorem Proving in Higher Order Logics. Springer Verlag; New York, Sept. 1998."},{"key":"16_CR12","unstructured":"J. O\u2019Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technical Journal, First Quarter 1999. Online at http:\/\/developer.intel.com\/technology\/itj\/ ."},{"key":"16_CR13","unstructured":"The omega project, 1999. http:\/\/www.ags.uni-sb.de\/projects\/deduktion\/ ."},{"key":"16_CR14","unstructured":"Proof and specification assisted design environments, ESPRIT LTR project 26241, 1999. http:\/\/www.dcs.gla.ac.uk\/prosper\/ ."},{"key":"16_CR15","volume-title":"Workshop on Computer-Aided Verification","author":"S. Rajan","year":"1996","unstructured":"S. Rajan, N. Shankar, and M. Srivas. An integration of model checking automated proof checking. In Workshop on Computer-Aided Verification. Springer Verlag; New York, 1996."},{"issue":"2","key":"16_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C. J. H. Seger","year":"1995","unstructured":"C. J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6(2):147\u2013189, Mar. 1995.","journal-title":"Formal Methods in System Design"},{"key":"16_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115:1\u201337, 1994.","journal-title":"Information and Computation"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1109\/HOL.1991.596282","volume-title":"International Workshop on the HOL Theorem Proving System and its Applications","author":"J. Wright von","year":"1991","unstructured":"J. von Wright. Mechanising the temporal logic of actions in HOL. In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors, International Workshop on the HOL Theorem Proving System and its Applications, pages 155\u2013159. IEEE Computer Society Press, Washington D. C., Aug. 1991."}],"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\/3-540-48153-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:02:27Z","timestamp":1558969347000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}