{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:19Z","timestamp":1750308559803,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,9,1]],"date-time":"2014-09-01T00:00:00Z","timestamp":1409529600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,9]]},"DOI":"10.1145\/2660540.2660982","type":"proceedings-article","created":{"date-parts":[[2014,10,31]],"date-time":"2014-10-31T19:32:56Z","timestamp":1414783976000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVS"],"prefix":"10.1145","author":[{"given":"Ariane Alves","family":"Almeida","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Bras\u00edlia, 70910-900 Bras\u00edlia, D.F., Brazil"}]},{"given":"Carlos H.","family":"Llanos","sequence":"additional","affiliation":[{"name":"Department of Mechanical Engineering, University of Bras\u00edlia, 70910-900 Bras\u00edlia, D.F., Brazil"}]},{"given":"Janier","family":"Arias-Garc\u00eda","sequence":"additional","affiliation":[{"name":"Department of Mechanical Engineering, University of Bras\u00edlia, 70910-900 Bras\u00edlia, D.F., Brazil"}]},{"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"additional","affiliation":[{"name":"Departments of Computer Science and Mathematics, University of Bras\u00edlia, 70910-900 Bras\u00edlia, D.F., Brazil"}]}],"member":"320","published-online":{"date-parts":[[2014,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"NASA LaRC PVS libraries. Avaliable at shemesh.larc.nasa.gov\/fm\/ftp\/larc\/PVS-library\/.  NASA LaRC PVS libraries. Avaliable at shemesh.larc.nasa.gov\/fm\/ftp\/larc\/PVS-library\/."},{"key":"e_1_3_2_1_2_1","first-page":"1","volume-title":"FPGA implementation of large-scale matrix inversion using single, double and custom floating-point precision,\" in VIII Southern Conf. on Programmable Logic (SPL)","author":"Arias-Garc\u00eda J.","year":"2012","unstructured":"J. Arias-Garc\u00eda , C. H. Llanos , M. Ayala-Rinc\u00f3n , and R. Jacobi , \" FPGA implementation of large-scale matrix inversion using single, double and custom floating-point precision,\" in VIII Southern Conf. on Programmable Logic (SPL) , 2012 , pp. 1 -- 6 . J. Arias-Garc\u00eda, C. H. Llanos, M. Ayala-Rinc\u00f3n, and R. Jacobi, \"FPGA implementation of large-scale matrix inversion using single, double and custom floating-point precision,\" in VIII Southern Conf. on Programmable Logic (SPL), 2012, pp. 1--6."},{"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","doi-asserted-by":"publisher","DOI":"10.1145\/1150343.1150379"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ReCoSoC.2012.6322907"},{"key":"e_1_3_2_1_6_1","first-page":"137","volume-title":"Encoding industrial hardware verification problems into effectively propositional logic,\" in Formal Methods in Computer-Aided Design (FMCAD)","author":"Emmer M.","year":"2010","unstructured":"M. Emmer , Z. Khasidashvili , K. Korovin , and A. Voronkov , \" Encoding industrial hardware verification problems into effectively propositional logic,\" in Formal Methods in Computer-Aided Design (FMCAD) , 2010 , pp. 137 -- 144 . M. Emmer, Z. Khasidashvili, K. Korovin, and A. Voronkov, \"Encoding industrial hardware verification problems into effectively propositional logic,\" in Formal Methods in Computer-Aided Design (FMCAD), 2010, pp. 137--144."},{"key":"e_1_3_2_1_7_1","first-page":"19","article-title":"Assigning Meaning to Programs,\" in Mathematical Aspects of Computer Science, ser. Proc, of Symposia in Applied Mathematics, no. 19","author":"Floyd R.","year":"1967","unstructured":"R. Floyd , \" Assigning Meaning to Programs,\" in Mathematical Aspects of Computer Science, ser. Proc, of Symposia in Applied Mathematics, no. 19 . AMS , 1967 , pp. 19 -- 32 . R. Floyd, \"Assigning Meaning to Programs,\" in Mathematical Aspects of Computer Science, ser. Proc, of Symposia in Applied Mathematics, no. 19. AMS, 1967, pp. 19--32.","journal-title":"AMS"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.003"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2014.21"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00010808"},{"key":"e_1_3_2_1_12_1","first-page":"128","volume-title":"Verifying equivalence of memories using a first order logic theorem prover,\" in Formal Methods in Computer-Aided Design (FMCAD)","author":"Khasidashvili Z.","year":"2009","unstructured":"Z. Khasidashvili , M. Kinanah , and A. Voronkov , \" Verifying equivalence of memories using a first order logic theorem prover,\" in Formal Methods in Computer-Aided Design (FMCAD) , 2009 , pp. 128 -- 135 . Z. Khasidashvili, M. Kinanah, and A. Voronkov, \"Verifying equivalence of memories using a first order logic theorem prover,\" in Formal Methods in Computer-Aided Design (FMCAD), 2009, pp. 128--135."},{"key":"e_1_3_2_1_13_1","volume-title":"dissertation","author":"Morra C.","year":"2010","unstructured":"C. Morra , \" A Flexible Framework for Hardware\/Software Design Space Exploration using Rewriting Logic,\" Ph. D. dissertation , Karlsruher Institut f\u00fcr Technologie , 2010 . C. Morra, \"A Flexible Framework for Hardware\/Software Design Space Exploration using Rewriting Logic,\" Ph.D. dissertation, Karlsruher Institut f\u00fcr Technologie, 2010."},{"key":"e_1_3_2_1_14_1","first-page":"25","volume-title":"FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations,\" in 15th International Conference on Field Programmable Logic and Applications (FPL)","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 International Conference on Field Programmable Logic and Applications (FPL) , 2005 , pp. 25 -- 30 . C. Morra, J. Becker, M. Ayala-Rinc\u00f3n, and R. Hartenstein, \"FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations,\" in 15th International Conference on Field Programmable Logic and Applications (FPL), 2005, pp. 25--30."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2008.37"},{"key":"e_1_3_2_1_16_1","volume-title":"SRI International Computer Science Laboratory","author":"Owre S.","year":"2001","unstructured":"S. Owre , N. Shankar , J. M. Rushby , and D. W. J. Stringer-Calvert , PVS System Guide , SRI International Computer Science Laboratory , 2001 . S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert, PVS System Guide, SRI International Computer Science Laboratory, 2001."}],"event":{"name":"SBCCI '14: 27th Symposium on Integrated Circuits and Systems Design","sponsor":["IEEE ICAS","SBC Brazilian Computer Society","IEEE Circuits and Systems Society","SIGDA ACM Special Interest Group on Design Automation","SBMICRO Brazilian Microelectronics Society"],"location":"Aracaju Brazil","acronym":"SBCCI '14"},"container-title":["Proceedings of the 27th Symposium on Integrated Circuits and Systems Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660540.2660982","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2660540.2660982","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:04:04Z","timestamp":1750273444000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660540.2660982"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9]]},"references-count":16,"alternative-id":["10.1145\/2660540.2660982","10.1145\/2660540"],"URL":"https:\/\/doi.org\/10.1145\/2660540.2660982","relation":{},"subject":[],"published":{"date-parts":[[2014,9]]},"assertion":[{"value":"2014-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}