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 :
https://search.ricest.ac.ir/dl/search/defaultta.aspx?DTC=49&DC=2351700
بازگشت