| 
|
Quote: compositional verification of memory safety in optimized code; encode low-level safety information via static single-assignment (SSA) proof variables
Topic:
type-safe and secure languages
Topic:
code optimization
Topic:
static single assignment; SSA
Quotation Skeleton
We present a verifiable low-level program representation to … and C#. Our representation precisely encodes safety information … [refs] proof variables that are first-class constructs in the program. We … (2) leverage existing compiler infrastructure to preserve safety … We also describe a simple type system that … our system enables compositional verification of memory safety … Google-1 Google-2
Copyright clearance needed for quotation.
Topic: type-safe and secure languages (43 items)
Topic: code optimization (54 items)
Topic: static single assignment; SSA (19 items)