Combining type-based analysis and model checking for finding counterexamples against non-interference