%0 Conference Paper %1 Clarke01boundedmodel %A Clarke, Edmund %A Biere, Armin %A Raimi, Richard %A Zhu, Yunshan %B Formal Methods in System Design %D 2001 %I Kluwer Academic Publishers %K modelchecking sat %P 2001 %T Bounded Model Checking Using Satisfiability Solving %U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.6391 %X The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.

@inproceedings{Clarke01boundedmodel, abstract = {The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.}, added-at = {2009-12-08T23:24:44.000+0100}, author = {Clarke, Edmund and Biere, Armin and Raimi, Richard and Zhu, Yunshan}, biburl = {https://www.bibsonomy.org/bibtex/2a55054c90c229bfbf73811113ecf4335/giuliano.losa}, booktitle = {Formal Methods in System Design}, description = {Bounded Model Checking Using Satisfiability Solving}, interhash = {8b70022a1524973a324662146bc15755}, intrahash = {a55054c90c229bfbf73811113ecf4335}, keywords = {modelchecking sat}, pages = 2001, publisher = {Kluwer Academic Publishers}, timestamp = {2009-12-08T23:24:44.000+0100}, title = {Bounded Model Checking Using Satisfiability Solving}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.6391}, year = 2001 }