Separation Logic Verification of C Programs with an SMT Solver (CROSBI ID 549033)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Botinčan, Matko ; Parkinson, Matthew ; Schulte, Wolfram
engleski
Separation Logic Verification of C Programs with an SMT Solver
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.
Separation logic; automated verification; automated theorem proving; C programming language
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
2009.
objavljeno
Podaci o matičnoj publikaciji
Proceedings of the 4th International Workshop on Systems Software Verification (SSV 09)
Huuck, Ralf ; Klein, Gerwin ; Schlich, Bastian
Elsevier
1571-0661
Podaci o skupu
4th International Workshop on Systems Software Verification (SSV 09)
predavanje
22.06.2009-24.06.2009
Aachen, Njemačka
Povezanost rada
Računarstvo, Matematika