Detail výsledku

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016). Electronic Proceedings in Theoretical Computer Science, EPTCS. Electronic Proceedings in Theoretical Computer Science. Brno: Faculty of Informatics MU, 2016. no. 233, p. 87-93. ISBN: 978-80-210-8362-2. ISSN: 2075-2180.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Charvát Lukáš, Ing., Ph.D.
Smrčka Aleš, Ing., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

Hades is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses onsingle-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.

Klíčová slova

automated tool, formal verification, pipeline-based microprocessors, data hazards

URL
Rok
2016
Strany
87–93
Časopis
Electronic Proceedings in Theoretical Computer Science, EPTCS, roč. 2016, č. 233, ISSN 2075-2180
Sborník
Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)
Řada
Electronic Proceedings in Theoretical Computer Science
Konference
MEMICS'16 Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
ISBN
978-80-210-8362-2
Vydavatel
Faculty of Informatics MU
Místo
Brno
DOI
10.4204/EPTCS.233.9
UT WoS
000390333200010
EID Scopus
2-s2.0-85018638270
BibTeX 
@inproceedings{BUT132606,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  booktitle="Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)",
  year="2016",
  series="Electronic Proceedings in Theoretical Computer Science",
  journal="Electronic Proceedings in Theoretical Computer Science, EPTCS",
  volume="2016",
  number="233",
  pages="87--93",
  publisher="Faculty of Informatics MU",
  address="Brno",
  doi="10.4204/EPTCS.233.9",
  isbn="978-80-210-8362-2",
  issn="2075-2180",
  url="http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9"
}
Soubory
Projekty
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru