Adrian J. Isles, Ramin Hojati, Robert K. Brayton: Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory. CAV 1998: 256-267