DocumentCode
2351700
Title
Verifying properties of hardware and software by predicate abstraction and model checking
Author
Bryant, Randal E. ; Rajamani, Sriram K.
Author_Institution
Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear
2004
fDate
7-11 Nov. 2004
Firstpage
437
Lastpage
438
Abstract
This tutorial describes automatic techniques for formally verifying hardware and software by creating Boolean abstractions of the underlying unbounded system state variables.
Keywords
Boolean functions; formal verification; hardware-software codesign; Boolean abstractions; decision procedures; formal verification; hardware property verification; model checking; predicate abstraction; software property verification; symbolic execution; underlying unbounded system state variables; Abstracts; Computer languages; Data analysis; Encoding; Formal verification; Hardware; Out of order; Random access memory; Simultaneous localization and mapping; Software systems;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Aided Design, 2004. ICCAD-2004. IEEE/ACM International Conference on
ISSN
1092-3152
Print_ISBN
0-7803-8702-3
Type
conf
DOI
10.1109/ICCAD.2004.1382615
Filename
1382615
Link To Document