Shortest Counterexamples for Symbolic Model Checking of LTL with Past.

Viktor Schuppan, Armin Biere

Browse the full TACAS paper archive.