Formal Verification of C Systems Code

J. Autom. Reasoning, pp. 125-187, 2009.

Cited by: 26|Views14
EI

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 abstraction, in par...More

Code:

Data:

Your rating :
0

 

Tags
Comments