Abstraction discovery and refinement for model checking by symbolic trajectory evaluation

Thesis

This dissertation documents two contributions to automating the formal verification of hardware – particularly memory-intensive circuits – by Symbolic Trajectory Evaluation (STE), a model checking technique based on symbolic simulation over abstract sets of states. The contributions focus on improvements to the use of BDD-based STE, which uses binary decision diagrams internally.

We introduce a solution to one of the major hurdles in using STE: finding suitable abstractions. Our wor...

Expand abstract

Authors: Adams, S

• Publication date: 2014
• DOI: 10.5287/ora-gj6qakdqd
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: formal verification; abstraction; symbolic trajectory evaluation; hardware verification; model checking
• Subjects: Theory and automated verification; Computing