Name
Abstract | ||
|---|---|---|
Verification for OO programs typically starts from a strongly typed object model in which distinct objects/fields are guaranteed not to overlap. This model simplifies verification by eliminating all ''uninteresting'' aliasing and allowing the use of more efficient frame axioms. Unfortunately, this model is unsound and incomplete for languages like C, where ''objects'' can overlap almost arbitrarily. Sound verification for C therefore typically starts from an untyped memory model, where memory is just an array of bytes. The untyped model, however, adds substantial annotation burden, and reasoning in the untyped model is computationally expensive. We propose a sound, typed semantics for C that provides the annotational and computational advantages of the typed object model while remaining sound and complete for C. We maintain a predicate identifying where the ''valid'' objects are, and introduce invariants and proof obligations that guarantee that the valid objects are suitably antialiased, and that (almost) all objects appearing in the program are valid. We describe the implementation of this approach in VCC (a sound verifier for C being used to verify the Microsoft Hypervisor) and the resulting performance gains. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1016/j.entcs.2009.09.061 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
sound verifier,valid object,efficient memory,c programming language,deductive program verification,sound verification,separated by commas.,memory models,untyped memory model,distinct object,please list keywords from your paper here,oo program,model simplifies verification,untyped model,object model,microsoft hypervisor,memory model | Byte,Programming language,Axiom,Computer science,Object model,Hypervisor,Theoretical computer science,Memory model,Invariant (mathematics),Predicate (grammar),Semantics | Journal |
Volume | ISSN | Citations |
254, | Electronic Notes in Theoretical Computer Science | 35 |
PageRank | References | Authors |
2.00 | 10 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ernie Cohen | 1 | 661 | 33.40 |
| Michał Moskal | 2 | 360 | 15.83 |
| Stephan Tobies | 3 | 1599 | 158.86 |
| Wolfram Schulte | 4 | 2342 | 153.40 |