Guided Model Checking with a Bayesian Meta-heuristic

Abstract. 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.

• Type: Conference
• Year: 2004
• Where: ACSD
• Authors: Kevin D. Seppi, Michael Jones, Peter Lamborn
• Keywords: ACSD 2004, Estimates Finds Errors, Formal Verification Algorithm, Hardware, Heuristic Estimates