Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Separation Logic Verification of C Programs with an SMT Solver

Matko Botincan, Matthew Parkinson, and Wolfram Schulte

Abstract

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

Publication typeInproceedings
Published inElectronic Notes in Theoretical Computer Science (ENTCS)
PublisherAssociation for Computing Machinery, Inc.
> Publications > Separation Logic Verification of C Programs with an SMT Solver