ABSTRACT
In this chapter, we will describe our smart predictive analysis technique tailored for enhancing the testing process of programs developed using the MCAPI specification. We have developed a trace-based SMT-driven (Satisfiability Modulo Theories) predictive analysis technique that reduces the process of explicitly enumerating and checking all interleavings to constraint solving that uses off-the-shelf SMT solvers. First, we instrument a program such that it produces a trace when executed. Given the program trace, we assemble a series of quantifier-free first-order logic (QF-FOL) formule that captures not only the given trace but also all possible interleavings of the events of this trace and the functional correctness properties of the program. The formula is fed to a solver; if the solver can find variable assignments that satisfy the formula, then we can find a valid permutation of the events in the trace (an execution scenario) that violates at least one correctness property. In this case, the SMT solver produces an abstract counterexample that embodies the erroneous execution. If not, we can presume that in all execution interleavings originating from the same set of events in the original trace, no violation of the correctness properties is possible.
