{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:01:49Z","timestamp":1765666909950},"publisher-location":"Berlin, Heidelberg","reference-count":14,"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_19","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T21:15:55Z","timestamp":1294434955000},"page":"200-215","source":"Crossref","is-referenced-by-count":16,"title":["Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving"],"prefix":"10.1007","author":[{"given":"Mike","family":"Gordon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joe","family":"Hurd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/10722167_40","volume-title":"Computer Aided Verification","author":"Y. Abarbanel","year":"2000","unstructured":"Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfsthal, Y.: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 538\u2013542. Springer, Heidelberg (2000), \n                    \n                      www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/ps\/checkers.ps"},{"key":"19_CR2","unstructured":"Accellera home page, \n                    \n                      http:\/\/www.accellera.org"},{"key":"19_CR3","unstructured":"Accellera Property Specification Lanuage Reference Manual, Version 1.0, \n                    \n                      http:\/\/www.eda.org\/vfv\/docs\/psl_lrm-1.0.pdf"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/10930755_11","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Amjad","year":"2003","unstructured":"Amjad, H.: Programming a symbolic model checker in a fully expansive theorem prover. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 171\u2013187. Springer, Heidelberg (2003)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Barras","year":"2000","unstructured":"Barras, B.: Programming and computing in HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 17\u201337. Springer, Heidelberg (2000)"},{"key":"19_CR6","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press\/McGraw-Hill, Cambridge, Massachusetts (1990)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.A. Dennis","year":"2000","unstructured":"Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The prosper toolkit. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 78\u201392. Springer, Heidelberg (2000)"},{"key":"19_CR8","unstructured":"The Accellera Formal Property Language Technical Committee home page, \n                    \n                      http:\/\/www.eda.org\/vfv"},{"key":"19_CR9","unstructured":"Comment on Ex 2, p 34, PSL RM v1.0, \n                    \n                      http:\/\/www.eda.org\/vfv\/hm\/1017.html"},{"key":"19_CR10","unstructured":"Reply to Comment on Ex 2, p 34, PSL RM v1.0, \n                    \n                      http:\/\/www.eda.org\/vfv\/hm\/1019.html"},{"key":"19_CR11","unstructured":"Gordon, M.J.C.: Validating the PSL\/Sugar semantics using automated reasoning. Formal Aspects of Computing. Special issue on Semantic Foundations of Engineering Design Languages (to appear)"},{"key":"19_CR12","unstructured":"Gordon, M.J.C.: Using HOL to study Sugar 2.0 semantics. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, volume CP-2002-211736 of NASA Conference Proceedings, pp. 87\u2013100 (2002), \n                    \n                      http:\/\/shemesh.larc.nasa.gov\/tphols2002\/proceedings.html"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055126","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 1\u201315. Springer, Heidelberg (1998)"},{"key":"19_CR14","unstructured":"Proposal Presented to the Accellera Formal Verification Technical Committee, \n                    \n                      http:\/\/www.haifa.il.ibm.com\/projects\/verification\/sugar\/Sugar_2.0_Accellera.ps"}],"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_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T10:00:14Z","timestamp":1553335214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}