We present a methodology for automated modular verification of C programs against specifications written in separation logic. Main features of our approach are a faithful representation of the C memory model and use of a SMT solver behind the separation logic prover. The methodology has been implemented in a prototype tool and used to automatically verify a number of annotated example C programs.

Details