Safety Property Verification Using Sequential SAT and Bounded Model Checking

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/MDT.2004.1277906

March/April 2004 (vol. 21 no. 2) pp. 132-143

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Ganapathy Parthasarathy Articles by Madhu K. Iyer Articles by Kwang-Ting (Tim) Cheng Articles by Li-C. Wang

	ASCII Text	x
	Ganapathy Parthasarathy, Madhu K. Iyer, Kwang-Ting (Tim) Cheng, Li-C. Wang, "Safety Property Verification Using Sequential SAT and Bounded Model Checking," IEEE Design and Test of Computers, vol. 21, no. 2, pp. 132-143, March/April, 2004.

	BibTex	x
	@article{ 10.1109/MDT.2004.1277906, author = {Ganapathy Parthasarathy and Madhu K. Iyer and Kwang-Ting (Tim) Cheng and Li-C. Wang}, title = {Safety Property Verification Using Sequential SAT and Bounded Model Checking}, journal ={IEEE Design and Test of Computers}, volume = {21}, number = {2}, issn = {0740-7475}, year = {2004}, pages = {132-143}, doi = {http://doi.ieeecomputersociety.org/10.1109/MDT.2004.1277906}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - MGZN JO - IEEE Design and Test of Computers TI - Safety Property Verification Using Sequential SAT and Bounded Model Checking IS - 2 SN - 0740-7475 SP132 EP143 EPD - 132-143 A1 - Ganapathy Parthasarathy, A1 - Madhu K. Iyer, A1 - Kwang-Ting (Tim) Cheng, A1 - Li-C. Wang, PY - 2004 VL - 21 JA - IEEE Design and Test of Computers ER -

Ganapathy Parthasarathy, University of California, Santa Barbara

Madhu K. Iyer, University of California, Santa Barbara

Kwang-Ting (Tim) Cheng, University of California, Santa Barbara

Li-C. Wang, University of California, Santa Barbara

The common view of model checking is as a supplementary methodology to improve the quality of simulation-based functional verification. Traditional model checking relies on BDD- or combinational-SAT-based approaches for search. The authors discuss the potential to apply a sequential SAT solver in model checking, comparing its performance against BDD- and combinational-SAT-based approaches.

Citation:

Ganapathy Parthasarathy, Madhu K. Iyer, Kwang-Ting (Tim) Cheng, Li-C. Wang, "Safety Property Verification Using Sequential SAT and Bounded Model Checking," IEEE Design and Test of Computers, vol. 21, no. 2, pp. 132-143, Mar./Apr. 2004, doi:10.1109/MDT.2004.1277906

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.