Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors.

Miroslav N. Velev

Published in: TACAS (2001)

Keyphrases

formal verification
bounded model checking
model checking
instruction set
computer architecture
symbolic model checking
automated verification
model checker
functional verification
fully automatic
semi automatic
program slicing
temporal logic
linear temporal logic
multi agent systems
high level
knowledge base