Formal verification of C systems code Structured types separation logic and theorem proving

Journal of Automated Reasoning, 2009.

Cited by: 8|Views17

Abstract:

Abstract Systems code is almost universally written in the C programming,language or a variant. C has a very low level of type and memory,abstraction and formal reasoning about C systems code requires a memory,model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstractio...More

Code:

Data:

Get fulltext within 24h
Bibtex
Your rating :
0

 

Tags
Comments