HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
The work
| Authors | Lukáš Charvát; Aleš Smrčka; Tomáš Vojnar |
|---|---|
| Editors | |
| Type | article |
| Year | 2016 |
| Citekey | charvat2016hades |
Where it appeared
| Published in | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Publisher | Open Publishing Association |
| Volume | 233 |
| Pages | 87--93 |
Identifiers
| arXiv | 1612.04986 from its oa_pdf_url |
|---|---|
| DOI | 10.4204/eptcs.233.9 |
| OpenAlex | W2562688732 |
Access
| Landing page | https://doi.org/10.4204/eptcs.233.9 |
|---|---|
| Free full text | https://arxiv.org/pdf/1612.04986 |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
HADES is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses on single-pipeline microprocessors designed at the register transfer level (RTL) and deals with read-after-write, write-after-write, and write-after-read hazards. HADES combines several techniques, including data-flow analysis, error pattern matching, SMT solving, and abstract regular model checking. It has been successfully tested on several microprocessors for embedded applications.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 11:13 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{charvat2016hades,
title = {HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems},
author = {Lukáš Charvát and Aleš Smrčka and Tomáš Vojnar},
year = {2016},
journal = {Electronic Proceedings in Theoretical Computer Science},
publisher = {Open Publishing Association},
volume = {233},
pages = {87--93},
doi = {10.4204/eptcs.233.9},
}
This record lives at https://refs.drheap.org/charvat2016hades/ and will keep doing so.