Pseudo-exhaustive testing uses the empirical observation that, for broad classes of software, a fault is likely triggered by only a few variables interacting. The method takes advantage of two relatively recent advances in software engineering: algorithms for efficiently generating covering arrays to represent software interaction test suites, and automated generation of test oracles using model checking. An experiment with a module of the Traffic Collision Avoidance System (TCAS) illustrates the approach testing pairwise through 6-way interactions. We also outline current and future work applying the test methodology to a large real-world application, the Personal Identity Verification (PIV) smart card.