Rishika Varma Kalidindi

Towards Tractable Hardware Model Validation Against Real Hardware

Verifying low-level system code requires reasoning about how software interacts with the hardware environment on which it runs. Typically, this means specifying an abstract model of the hardware and verifying the code against it. However, the validity of the verification result depends on the accuracy of the formalized...