{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:33Z","timestamp":1761611193518,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,8,28]]},"DOI":"10.1145\/1150343.1150379","type":"proceedings-article","created":{"date-parts":[[2006,10,18]],"date-time":"2006-10-18T22:04:00Z","timestamp":1161209040000},"page":"125-130","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["SAEPTUM"],"prefix":"10.1145","author":[{"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"first","affiliation":[{"name":"Universidade de Bras\u00edlia, Bras\u00edlia, Brazil"}]},{"given":"Thomas M.","family":"Sant'Ana","sequence":"additional","affiliation":[{"name":"Universidade de Bras\u00edlia, Bras\u00edlia, Brazil"}]}],"member":"320","published-online":{"date-parts":[[2006,8,28]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of Design and Application of Strategies\/Tactics in Higher Order Logics STRATA'03","author":"Archer M.","year":"2003","unstructured":"M. Archer , B. D. Vito , and C. Mu\u00f1oz . Developing user strategies in PVS: A tutorial . In Proceedings of Design and Application of Strategies\/Tactics in Higher Order Logics STRATA'03 , NASA\/CP- 2003 -212448, 2003. M. Archer, B. D. Vito, and C. Mu\u00f1oz. Developing user strategies in PVS: A tutorial. In Proceedings of Design and Application of Strategies\/Tactics in Higher Order Logics STRATA'03, NASA\/CP-2003-212448, 2003."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.768501"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142155.1142156"},{"key":"e_1_3_2_1_4_1","volume-title":"2nd Int.Workshop on Reduction Strategies in Rewriting And Programming","volume":"141","author":"Ayala-Rinc\u00f3n M.","year":"2002","unstructured":"M. Ayala-Rinc\u00f3n , R. M. Neto , R. P. Jacobi , C. Llanos , and R. Hartenstein . Applying ELAN strategies in simulation processors over simple architectures . In 2nd Int.Workshop on Reduction Strategies in Rewriting And Programming , volume 70(6) of ENTCS, pages 127-- 141 . Elsevier , 2002 . M. Ayala-Rinc\u00f3n, R. M. Neto, R. P. Jacobi, C. Llanos, and R. Hartenstein. Applying ELAN strategies in simulation processors over simple architectures. In 2nd Int.Workshop on Reduction Strategies in Rewriting And Programming, volume 70(6) of ENTCS, pages 127--141. Elsevier, 2002."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1383-7621(03)00073-0"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054101000412"},{"key":"e_1_3_2_1_7_1","volume-title":"Fourth Workshop on Rewriting Logic and its Applications, WRLA '02","author":"Eker S.","year":"2002","unstructured":"S. Eker , J. Meseguer , and A. Sridharanarayanan . The Maude LTL model checker. In F. Gadducci and U. Montanari, editors , Fourth Workshop on Rewriting Logic and its Applications, WRLA '02 , volume~71 of ENTCS. Elsevier , 2002 . S. Eker, J. Meseguer, and A. Sridharanarayanan. The Maude LTL model checker. In F. Gadducci and U. Montanari, editors, Fourth Workshop on Rewriting Logic and its Applications, WRLA '02, volume~71 of ENTCS. Elsevier, 2002."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.833614"},{"issue":"3","key":"e_1_3_2_1_9_1","first-page":"543","volume":"4","author":"Jacobi R. P.","year":"2005","unstructured":"R. P. Jacobi , M. Ayala-Rinc\u00f3n , L. G. A. Carvalho , C. Llanos , and R. Hartenstein . Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. Genetics and Mol. Research , 4 ( 3 ): 543 -- 552 , 2005 . R. P. Jacobi, M. Ayala-Rinc\u00f3n, L. G. A. Carvalho, C. Llanos, and R. Hartenstein. Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. Genetics and Mol. Research, 4(3):543--552, 2005.","journal-title":"Genetics and Mol. Research"},{"key":"e_1_3_2_1_10_1","series-title":"LNCS","first-page":"103","volume-title":"Proc. 17th FSTTCS","author":"Kapur D.","year":"1997","unstructured":"D. Kapur and M. Subramaniam . Mechanizing Verification of Arithmetic Circuits: SRT Division . In Proc. 17th FSTTCS , volume 1346 of LNCS , pages 103 -- 122 . Springer , 1997 . D. Kapur and M. Subramaniam. Mechanizing Verification of Arithmetic Circuits: SRT Division. In Proc. 17th FSTTCS, volume 1346 of LNCS, pages 103--122. Springer, 1997."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00010808"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/968486.968488"},{"key":"e_1_3_2_1_13_1","unstructured":"M. P. M. Clavel. The ITP Tool's Manual. U. Complutense de Madrid http:\/\/maude.sip.ucm.es\/itp\/ April 2005.  M. P. M. Clavel. The ITP Tool's Manual. U. Complutense de Madrid http:\/\/maude.sip.ucm.es\/itp\/ April 2005."},{"key":"e_1_3_2_1_14_1","volume-title":"Technical report","author":"McCombs T.","year":"2003","unstructured":"T. McCombs . M AUDE 2.0 Primer Version 1.0. Technical report , University of Illinois at Urbana-Champaign , 2003 . Available: http:\/\/maude.cs.uiuc.edu\/primer. T. McCombs. MAUDE 2.0 Primer Version 1.0. Technical report, University of Illinois at Urbana-Champaign, 2003. Available: http:\/\/maude.cs.uiuc.edu\/primer."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/527212.837427"},{"key":"e_1_3_2_1_16_1","first-page":"25","volume-title":"FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations. In 15th Int. Conf. on Field Programmable Logic and App.","author":"Morra C.","year":"2005","unstructured":"C. Morra , J. Becker , M. Ayala-Rinc\u00f3n , and R. Hartenstein . FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations. In 15th Int. Conf. on Field Programmable Logic and App. , pages 25 -- 30 . IEEE CS, 2005 . C. Morra, J. Becker, M. Ayala-Rinc\u00f3n, and R. Hartenstein. FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations. In 15th Int. Conf. on Field Programmable Logic and App., pages 25--30. IEEE CS, 2005."},{"key":"e_1_3_2_1_17_1","volume-title":"NIA-NASA Langley","author":"Mu\u00f1oz C.","year":"2003","unstructured":"C. Mu\u00f1oz . Rapid prototyping in PVS. Report NIA No. 2003-03 and NASA\/CR-2003-212418 , NIA-NASA Langley , National Institute of Aerospace , Hampton, VA , May 2003 . C. Mu\u00f1oz. Rapid prototyping in PVS. Report NIA No. 2003-03 and NASA\/CR-2003-212418, NIA-NASA Langley, National Institute of Aerospace, Hampton, VA, May 2003."},{"key":"e_1_3_2_1_18_1","volume-title":"U. of Illinois at Urbana-Champaign","author":"Mart\u00ed-Oliet J. M. N.","year":"2003","unstructured":"J. M. N. Mart\u00ed-Oliet and M. Palomino . Notes on Model Checking and Abstraction in Rewriting Logic. Technical report , U. of Illinois at Urbana-Champaign , 2003 . Available: http:\/\/maude.cs.uiuc.edu\/papers\/. J. M. N. Mart\u00ed-Oliet and M. Palomino. Notes on Model Checking and Abstraction in Rewriting Logic. Technical report, U. of Illinois at Urbana-Champaign, 2003. Available: http:\/\/maude.cs.uiuc.edu\/papers\/."},{"key":"e_1_3_2_1_19_1","series-title":"LNCS","first-page":"258","volume-title":"Theorem Provers in Circuit Design (TPCD '94)","author":"Owre S.","year":"1994","unstructured":"S. Owre , J. M. Rushby , N. Shankar , and M. K. Srivas . A tutorial on using PVS for hardware verification . In Theorem Provers in Circuit Design (TPCD '94) , volume 901 of LNCS , pages 258 -- 279 . Springer , 1994 . S. Owre, J. M. Rushby, N. Shankar, and M. K. Srivas. A tutorial on using PVS for hardware verification. In Theorem Provers in Circuit Design (TPCD '94), volume 901 of LNCS, pages 258--279. Springer, 1994."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024716316140"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/646528.695049"},{"key":"e_1_3_2_1_22_1","volume-title":"Workshop on Formal Techniques for Hardware and Hardware-like Systems","author":"Shen X.","year":"1998","unstructured":"X. Shen and Arvind. Design and verification of speculative processors . In Workshop on Formal Techniques for Hardware and Hardware-like Systems , Marstrand, Sweden , June 1998 . X. Shen and Arvind. Design and verification of speculative processors. In Workshop on Formal Techniques for Hardware and Hardware-like Systems, Marstrand, Sweden, June 1998."}],"event":{"name":"SBCCI06: 19th Symposium on Integrated Circuits and System Design","sponsor":["ACM Association for Computing Machinery","SIGDA ACM Special Interest Group on Design Automation"],"location":"Ouro Preto MG Brazil","acronym":"SBCCI06"},"container-title":["Proceedings of the 19th annual symposium on Integrated circuits and systems design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1150343.1150379","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,8]],"date-time":"2023-01-08T01:48:49Z","timestamp":1673142529000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1150343.1150379"}},"subtitle":["verification of\n            <i>ELAN<\/i>\n            hardware specifications using the proof assistant\n            <i>PVS<\/i>"],"short-title":[],"issued":{"date-parts":[[2006,8,28]]},"references-count":22,"alternative-id":["10.1145\/1150343.1150379","10.1145\/1150343"],"URL":"https:\/\/doi.org\/10.1145\/1150343.1150379","relation":{},"subject":[],"published":{"date-parts":[[2006,8,28]]},"assertion":[{"value":"2006-08-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}