| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 421972 | Electronic Notes in Theoretical Computer Science | 2009 | 19 Pages |
Abstract
This paper presents a methodology for automated modular verification of C programs against specifications written in separation logic. The distinguishing features of the approach are representation of the C memory model in separation logic by means of rewrite rules suitable for automation and the careful integration of an SMT solver behind the separation logic prover to guide the proof search.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
