Article,
Specification-based Verification of Incomplete Programs
ACEEE International Journal on Information Technology, 2 (2): 6 (April 2012)
Abstract
Recently, formal methods like model checking or
theorem proving have been considered efficient tools for
software verification. However, when practically applied, those
techniques suffer high complexity cost. Combining static
analysis with dynamic checking to deal with this problem has
been becoming an emerging trend, which results in the
introduction of concolic testing technique and its variations.
However, the analysis-based verification techniques always
assume the availability of full source code of the verified
program, which does not always hold in real life contexts. In
this paper, we propose an approach to tackle this problem,
where our contributed ideas are (i) combining function
specification with control flow analysis to deal with sourcemissing
function; (ii) generating self-complete programs from
incomplete programs by means of concrete execution, thus
making them fully verifiable by model checking; and (iii)
developing a constraint-based test-case generation technique
to significantly reduce the complexity. Our solution has been
proved viable when successfully deployed for checking
programming work of students.
