Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. - Lukás Charvát; Ales Smrcka; Tomás Vojnar (MTV, 2012)

An Abstraction of Multi-port Memories with Arbitrary Addressable Units. - Lukás Charvát; Ales Smrcka; Tomás Vojnar (EUROCAST (1), 2013)

Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. - Lukás Charvát; Ales Smrcka; Tomás Vojnar (MTV, 2014)

Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems. - Lukás Charvát; Ales Smrcka; Tomás Vojnar (EUROCAST, 2015)

HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. - Lukás Charvát; Ales Smrcka; Tomás Vojnar (MEMICS, 2016)

Automatická verifikace v procesu soubežného návrhu hardware a software ; Automated Verification in HW/SW Co-design. - Lukás Charvát (2020)

Utilizing parametric systems for detection of pipeline hazards. - Lukás Charvát; Ales Smrcka; Tomás Vojnar (Int. J. Softw. Tools Technol. Transf., 2022)