The Oracle Problem for Testing against Quantified Properties

The oracle problem for testing from quantified proper- ties is discussed and illustrated by proposed solutions for first-order logic and computation tree logic (CTL) proper- ties. Unless constraints are placed, it is not always possible to generate feasible test suites from which accurate conclu- sions on their execution results can be reached regarding conformity with the intended property.