_id,doi,title 4394,1552,Using First-Order Theorem Provers in the Jahob Data Structure Verification System