Concurrent Program Verification with Lazy Sequentialization and Interval Analysis