Efficient Sequentialization for Concurrent Program Verification