{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:04Z","timestamp":1750308664855,"version":"3.41.0"},"publisher-location":"New York, New York, USA","reference-count":17,"publisher":"ACM Press","license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1145\/1275571.1275583","type":"proceedings-article","created":{"date-parts":[[2016,3,25]],"date-time":"2016-03-25T12:48:51Z","timestamp":1458910131000},"page":"9-es","source":"Crossref","is-referenced-by-count":0,"title":["Introduction to formal processor verification at logic level"],"prefix":"10.1145","author":[{"given":"Paul","family":"Amblard","sequence":"first","affiliation":[{"name":"Universit\u00e9 Joseph Fourier, Grenoble, France"}]},{"given":"Fabienne","family":"Lagnier","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Joseph Fourier, Grenoble, France"}]},{"given":"Michel","family":"Levy","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Joseph Fourier, Grenoble, France"}]}],"member":"320","reference":[{"key":"key-10.1145\/1275571.1275583-1","unstructured":"<b>S. B. Akers:<\/b> Binary Decision Diagrams, IEEE Transactions on Computers, Vol C-27, June 1978."},{"key":"key-10.1145\/1275571.1275583-2","unstructured":"<b>P. Amblard, J. C. Fernandez, F. Lagnier, F. Maraninchi, P. Sicard et P. Waille:<\/b>Architectures Logicielles et Matérielles, Dunod, 2000 (in french)."},{"key":"key-10.1145\/1275571.1275583-3","doi-asserted-by":"crossref","unstructured":"<b>P. Amblard, F. Lagnier and M. Levy:<\/b> Introducing Digital Circuits Design and Verification Concurrently, Proceedings of the 3<sup>rd<\/sup> European Workshop on Microelectronics Education, Aix en Provence, 18--19 May 2000, Kluwer, pp 261--264.","DOI":"10.1007\/978-94-015-9506-3_60"},{"key":"key-10.1145\/1275571.1275583-4","doi-asserted-by":"crossref","unstructured":"<b>N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud:<\/b> The Synchronous Data-flow Programming Language Lustre, Proceedings of the IEEE, pp 1305--1320, September 1991.","DOI":"10.1109\/5.97300"},{"key":"key-10.1145\/1275571.1275583-5","doi-asserted-by":"crossref","unstructured":"<b>N. Halbwachs, F. Lagnier and C. Ratel:<\/b> Programming and Verifying Real-time Systems by Means of the Synchronous Data-flow Programming Language Lustre, IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, September 1992, pp 785--793.","DOI":"10.1109\/32.159839"},{"key":"key-10.1145\/1275571.1275583-6","doi-asserted-by":"crossref","unstructured":"<b>N. Halbwachs:<\/b>Synchronous programming of reactive systems, Kluwer Academic Pub., 1993","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"key-10.1145\/1275571.1275583-7","unstructured":"<b>M. Levy, L. Trilling:<\/b> A PVS-Based Approach for Teaching Constructing Correct Iterations FM'99 (Formal Methods), LNCS 1709, pp 1859--1860"},{"key":"key-10.1145\/1275571.1275583-8","unstructured":"<b>R. Paul:<\/b>SPARC Architecture Assembly Language Programming, and C, Prentice-Hall, Inc., 1994"},{"key":"key-10.1145\/1275571.1275583-9","unstructured":"<b>Sima D., Fountain and Kacsuk<\/b>Advanced Computer Architectures, 1997, Addison-Wesley"},{"key":"key-10.1145\/1275571.1275583-10","unstructured":"<b>M. Velev:<\/b> Integrating Formal Verification into an Advanced Computer Architecture Course, ASEE 2003 Annual Conference, http:\/\/www.ece.cmu.edu\/~mvelev\/ASEE03.pdf"},{"key":"key-10.1145\/1275571.1275583-11","unstructured":"<b>N. Wirth:<\/b>Digital Circuit Design, Springer-Verlag, 1995."},{"key":"key-10.1145\/1275571.1275583-12","unstructured":"I.E.E.E Micro, may-june 2000, Computer Architecture Education."},{"key":"key-10.1145\/1275571.1275583-13","unstructured":"The SPARC Architecture Manual, version 8, Prentice-Hall, Inc., 1992."},{"key":"key-10.1145\/1275571.1275583-14","unstructured":"http:\/\/www.estec.esa.nl\/wsmwww\/leon\/leon.html"},{"key":"key-10.1145\/1275571.1275583-15","unstructured":"http:\/\/www.sparc.com\/standards\/V8.pdf"},{"key":"key-10.1145\/1275571.1275583-16","unstructured":"http:\/\/www-verimag.imag.fr\/ SYNCHRONE"},{"key":"key-10.1145\/1275571.1275583-17","unstructured":"http:\/\/tima-cmp.imag.fr\/~amblard\/EXAMS\/exams.html"}],"event":{"name":"the 2004 workshop","start":{"date-parts":[[2004,6,19]]},"number":"WCAE 2004","theme":"held in conjunction with the 31st International Symposium on Computer Architecture","location":"Munich, Germany","acronym":"WCAE '04"},"container-title":["Proceedings of the 2004 workshop on Computer architecture education held in conjunction with the 31st International Symposium on Computer Architecture - WCAE '04"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275571.1275583","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/dl.acm.org\/ft_gateway.cfm?id=1275583&ftid=435900&dwn=1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:31Z","timestamp":1750276831000},"score":1,"resource":{"primary":{"URL":"http:\/\/dl.acm.org\/citation.cfm?doid=1275571.1275583"}},"subtitle":["a case study"],"proceedings-subject":"Computer architecture education","short-title":[],"issued":{"date-parts":[[2004]]},"references-count":17,"URL":"https:\/\/doi.org\/10.1145\/1275571.1275583","relation":{},"subject":[],"published":{"date-parts":[[2004]]}}}