摘要 : Abstract In order to prove conformance to memory standards and bound memory access latency, recently proposed real-time DRAM controllers rely on paper and pencil proofs, which can be troubling: they are difficult to read and revie... 展开
作者 | Felipe Lisboa Malaquias Mihail Asavoae Florian Brandner |
---|---|
作者单位 | |
期刊名称 | 《Real-time systems》 |
页码/总页数 | 664-704 / 41 |
语种/中图分类号 | 英语 / TP3 |
关键词 | DRAM Memory controller Coq Formal proof assistant |
DOI | 10.1007/s11241-023-09411-3 |
馆藏号 | TP-197 |