Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Marked Items 
Alerts
Order History
Saved Items
All
Favorites
    
Book Chapter Printable view
Comparing SAT Encodings for Model Checking

Comparing SAT Encodings for Model Checking

Book SeriesLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN0302-9743 (Print) 1611-3349 (Online)
VolumeVolume 2239/2001
BookPrinciples and Practice of Constraint Programming — CP 2001
DOI10.1007/3-540-45578-7
Copyright2001
ISBN978-3-540-42863-3
DOI10.1007/3-540-45578-7_82
Page784
Subject CollectionComputer Science
SpringerLink DateMonday, January 01, 2001
Add to marked items

Comparing SAT Encodings for Model Checking

Daniel Sheridan5 Contact Information

(5)  Artificial Intelligence Group Department of Computer Science, University of York, York, England
Abstract
Bounded model checking (BMC) [1] was proposed as a solution to some of the problems (e.g. space explosion) of conventional BDD-based symbolic model checking by introducing a temporal bound. The problem can then be encoded as a Boolean formula and used as input to a SAT checker: the output of a BMC tool is a conjunction of state transition functions and state verification functions.

Contact Information Daniel Sheridan
Email: djs@cs.york.ac.uk
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.
more options
Find


Export this chapter
Export this chapter as RIS | Text
 
Frequently asked questions | General information on journals and books | Send us your feedback | Impressum | Contact
© Springer. Part of Springer Science+Business Media
Privacy, Disclaimer, Terms and Conditions, © Copyright Information
Remote Address: 38.107.191.109 • Server: mpweb22
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)