Conference paper

CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. 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). Sydney: School of Computer Science and Engineering, University of New South Wales, 2016, pp. 87-93. ISSN 2075-2180. Available from: http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9
Publication language:english
Original title:Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Title (cs):Hades: analýza hazardů v mikroprocesorech s využitím formální verifikace parametrických systémů
Pages:87-93
Proceedings:Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)
Conference:MEMICS'16 - 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Series:Electronic Proceedings in Theoretical Computer Science
Place:Sydney, AU
Year:2016
URL:http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9
Journal:Electronic Proceedings in Theoretical Computer Science, Vol. 2016, No. 233, Sydney, AU
ISSN:2075-2180
Publisher:School of Computer Science and Engineering, University of New South Wales
Files: 
+Type Name Title Size Last modified
icon1612.04986.pdf475 KB2017-02-23 15:10:10
^ Select all
With selected:
Keywords
automated tool, formal verification, pipeline-based microprocessors, data hazards
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   author = {Luk{\'{a}}{\v{s}} Charv{\'{a}}t and Ale{\v{s}} Smr{\v{c}}ka
	and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Hades: Microprocessor Hazard Analysis via Formal
	Verification of Parameterized Systems},
   pages = {87--93},
   booktitle = {Proceedings 11th Doctoral Workshop on Mathematical and
	Engineering Methods in Computer Science (MEMICS 2016)},
   series = {Electronic Proceedings in Theoretical Computer Science},
   journal = {Electronic Proceedings in Theoretical Computer Science},
   volume = {2016},
   number = {233},
   year = {2016},
   location = {Sydney, AU},
   publisher = {School of Computer Science and Engineering, University of
	New South Wales},
   ISSN = {2075-2180},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso-8859-2?id=11312}
}

Your IPv4 address: 54.81.6.121
Switch to IPv6 connection

DNSSEC [dnssec]