Formal verification with functional indeterminacy on the basis of satisfiability testing of the conjunctive normal form
Liudmila D. Cheremisinova, D. Ya. Novikov · Automatic Control and Computer Sciences · 2010
The verification problem for the case of the description of a functional indeterminacy set by a system of partially specified Boolean functions is considered. The formal approach based on the reduction of the verification problem to a satisfiability test of the conjunctive normal form is suggested. Three approaches to the solution of the verification problem based on sequential, simultaneous, and group testing of multi-output intervals of the system of partially specified Boolean functions are investigated.