| 
|
Quote: proof-carrying code by computing the safety predicate and a checkable proof; Floyd's verification conditions
topics >
all references >
references m-o >
Topic:
type-safe and secure languages
Topic:
proof-carrying code
Topic:
program proof via assertions
Quotation Skeleton
Our technique is based on Floyd's verification conditions … [Schwartz (ed), Mathematical Aspects of Computer Science, 1967] … of safety invariants. … Certification of programs involves two steps: 1. Compute … 2. Generate a proof of the safety predicate, … To compute the safety predicate, we first generate … [for non-loop programs] the verification-condition VC_0 for the beginning of … toward the beginning. … [p. 235] To validate the [PCC] binary, the code … computes its safety predicate using the VC rules. … Google-1 Google-2
Copyright clearance needed for quotation.
Topic: type-safe and secure languages (42 items)
Topic: proof-carrying code (7 items)
Topic: program proof via assertions (61 items)