Kenneth L. McMillan, Nina Amla: Automatic Abstraction without Counterexamples. TACAS 2003: 2-17
Kenneth L. McMillan: Applying SAT Methods in Unbounded Symbolic Model Checking. CAV 2002: 250-264
Benchmarks used in the following publications are available online:
Kenneth L. McMillan: Lazy Annotation for Program Testing and Verification. CAV 2010