{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T07:44:33Z","timestamp":1743493473019},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2003,12,1]],"date-time":"2003-12-01T00:00:00Z","timestamp":1070236800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2003,12]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>The Accellera organisation selected Sugar, IBM\u2019s formal specification language, as the basis for a standard to \u2018drive assertion-based verification\u2019 in the electronics industry. Sugar combines regular expressions, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) into a property language intended for both static verification (e.g. model checking) and dynamic verification (e.g. simulation). In 2003 Accellera decided to rename the evolving standard to \u2018Accellera Property Specification Language\u2019 (or \u2018PSL\u2019 for short). We motivate and describe a deep semantic embedding of PSL in the version of higher-order logic supported by the HOL 4 theorem-proving system. The main goal of this paper is to demonstrate that mechanised theorem proving can be a useful aid to the validation of the semantics of an industrial design language.<\/jats:p>","DOI":"10.1007\/s00165-003-0014-5","type":"journal-article","created":{"date-parts":[[2003,12,23]],"date-time":"2003-12-23T20:14:14Z","timestamp":1072210454000},"page":"406-421","source":"Crossref","is-referenced-by-count":12,"title":["Validating the PSL\/Sugar Semantics Using Automated Reasoning"],"prefix":"10.1145","volume":"15","author":[{"given":"Michael J. C.","family":"Gordon","sequence":"first","affiliation":[{"name":"University of Cambridge Computer Laboratory, William Gates Building, J. J. Thomson Avenue, CB3 0FD, Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"Proceeding of the 12th International Conference on Computer Aided Verification (CAV), LNCS 1855","author":"Abarbanel Y.","year":"2000"},{"key":"p_2","unstructured":"[Acc] Accellera Property Specification Language Reference Manual Version 1.01. At http:\/\/www.eda.org\/vfv\/docs\/psl_ lrm-1.01.pdf."},{"key":"p_3","volume-title":"Proceeding of the 13th International Conference on Computer Aided Verification (CAV), LNCS 2102","author":"Beer I.","year":"2001"},{"key":"p_4","first-page":"129","volume-title":"Theorem Provers in Circuit Design: Proceedings of the IFIP TC10\/WG 10.2 International Conference, Nijmegen","author":"Boulton R.","year":"1992"},{"key":"p_5","volume-title":"VhdlCohen","author":"Coh","year":"2003"},{"key":"p_6","volume-title":"March","author":"Ei","year":"2002"},{"key":"p_7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36576-1","volume-title":"Proceeding of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME","author":"Gordon M.","year":"2003"},{"key":"p_8","volume-title":"editors","author":"Go","year":"1993"},{"key":"p_9","series-title":"Lecture Notes in Computer Science","first-page":"234","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs","author":"Har","year":"2000"},{"key":"p_10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/BFb0036915","volume-title":"Proceedings of the 10th International Colloquium on Automata, Languages and Programming","author":"Halpern J.","year":"1983"},{"key":"p_11","volume-title":"Software Technology Research Laboratory","author":"Cau A."},{"key":"p_12","unstructured":"[Mat] W3C Math Home. At http:\/\/www.w3.org\/Math."},{"key":"p_13","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002"},{"key":"p_14","unstructured":"[Ope] OpenMath website. At http:\/\/www.openmath.org."},{"key":"p_15","doi-asserted-by":"crossref","unstructured":"[RSS95] \n      Rajan S. Shankar N.\n     and \n      Srivas M. K\n  .: \n  An integration of model-checking with automated proof checking\n  . In P. Wolper editor Computer-Aided Verification CAV\n   '95 volume \n  939\n   of \n  Lecture Notes in Computer Science Liege Belgium June \n  1995\n  . \n  Springer pp. \n  84\n  -\n  97","DOI":"10.1007\/3-540-60045-0_42"},{"key":"p_16","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs99), number 1690 in Lecture Notes in Computer Science","author":"Sc","year":"1999"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-003-0014-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-003-0014-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-003-0014-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:39:42Z","timestamp":1641483582000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-003-0014-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,12]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2003,12]]}},"alternative-id":["10.1007\/s00165-003-0014-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-003-0014-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,12]]}}}