This paper presents a formal verification algorithm for finding errors in models of complex concurrent systems. The algorithm improves explicit guided model checking by applying the empirical Bayes method to revise heuristic estimates of the distance from a given state to an error state. Guided search using the revised estimates finds errors with less search effort than the original estimates.

Pdf version or through the ACM Portal.

Seppi, K., Jones, M., and Lamborn, P. 2005. Guided model checking with a Bayesian meta-heuristic. Fundam. Inf. 70, 1 (Oct. 2005), 111-126.

@article{1151666,
   author = {Seppi,, Kevin and Jones,, Michael and Lamborn,, Peter},
   title = {Guided model checking with a Bayesian meta-heuristic},
   journal = {Fundam. Inf.},
   volume = {70},
   number = {1},
   year = {2005},
   issn = {0169-2968},
   pages = {111--126},
   publisher = {IOS Press},
   address = {Amsterdam, The Netherlands, The Netherlands},
}