A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. - Yonit Kesten; Amit Klein 001; Amir Pnueli; Gil Raanan (World Congress on Formal Methods, 1999)