{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,26]],"date-time":"2026-03-26T15:17:18Z","timestamp":1774538238782,"version":"3.50.1"},"reference-count":28,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T00:00:00Z","timestamp":1631750400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T00:00:00Z","timestamp":1631750400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T00:00:00Z","timestamp":1631750400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,9,16]]},"DOI":"10.1109\/vdat53777.2021.9601109","type":"proceedings-article","created":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T23:41:04Z","timestamp":1636587664000},"page":"1-6","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification and Analysis of a Pseudo Random Number Generator"],"prefix":"10.1109","author":[{"given":"David","family":"Selvakumar","sequence":"first","affiliation":[]},{"given":"J","family":"Mervin","sequence":"additional","affiliation":[]},{"given":"Shashikala","family":"Pattanshetty","sequence":"additional","affiliation":[]},{"given":"D","family":"Vivian","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","year":"0","journal-title":"Bounded Model Checking Software"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"ref12","year":"0","journal-title":"The Foundational Cryptography Framework"},{"key":"ref13","year":"0"},{"key":"ref14","year":"0","journal-title":"The Coq Proof Assistant"},{"key":"ref15","author":"balasch","year":"2018","journal-title":"2018 IEEE 23rd European Test Symposium (ETS)"},{"key":"ref16","author":"haddad","year":"0","journal-title":"Workshop on Cryptographic Hardware and Embedded Systems CHES 2015"},{"key":"ref17","author":"d\u00f6rre","year":"0","journal-title":"Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS &#x2018;16)"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29613-5_4"},{"key":"ref19","year":"0"},{"key":"ref28","year":"0","journal-title":"NIST SP800-90B Entropy Sources Used for Random Bit Generation"},{"key":"ref4","year":"0","journal-title":"Cryptol Language of Crypto"},{"key":"ref27","year":"0","journal-title":"NIST SP-800-90C Random Bit Generator (RBG) Constructions"},{"key":"ref3","year":"0","journal-title":"Software Analysis Work Bench"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ISVLSI.2015.107"},{"key":"ref5","article-title":"Sequential Equivalence Verification","year":"0"},{"key":"ref8","year":"0","journal-title":"Model Checker for Hardware Designs"},{"key":"ref7","year":"0","journal-title":"A Verilog to C Translator Tool"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2017.54"},{"key":"ref9","author":"mukherjee","year":"0","journal-title":"Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)"},{"key":"ref1","article-title":"A Formally Verified Crypto Extension to a RISC-V Proc","author":"joseph","year":"0"},{"key":"ref20","year":"0","journal-title":"NIST SP - 800-22 Test Suite"},{"key":"ref22","year":"0","journal-title":"The NIST SP 800-90A deterministic random bit generator validation system (DRBGVS)"},{"key":"ref21","first-page":"368","author":"clarke","year":"0","journal-title":"Proc &#x2019;03 DAC"},{"key":"ref24","author":"edmund","year":"2003","journal-title":"Technical Report"},{"key":"ref23","first-page":"1","author":"bahadur","year":"16","journal-title":"2016 VLSI-SATA"},{"key":"ref26","year":"0","journal-title":"Random Number Generation Using DRBG NIST SP 800-90Ar1"},{"key":"ref25","year":"0","journal-title":"AIS-31 Test Suite"}],"event":{"name":"2021 25th International Symposium on VLSI Design and Test (VDAT)","location":"Surat, India","start":{"date-parts":[[2021,9,16]]},"end":{"date-parts":[[2021,9,18]]}},"container-title":["2021 25th International Symposium on VLSI Design and Test (VDAT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9600867\/9600899\/09601109.pdf?arnumber=9601109","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T16:50:52Z","timestamp":1652201452000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9601109\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,16]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/vdat53777.2021.9601109","relation":{},"subject":[],"published":{"date-parts":[[2021,9,16]]}}}