Name
Abstract | ||
|---|---|---|
First-class function pointers are common in low-level assembly languages. Higher-level features such as closures, virtual functions, and call-backs are all compiled down to assembly code with function pointers. Function pointers are, however, hard to reason about. Previous program logics for certifying assembly programs either do not support first-class function pointers, or follow Continuation-Passing-Style reasoning which does not provide the same partial correctness guarantee as in high-level languages. In this paper, we present a simple semantic model for certifying the partial correctness property of assembly programs with first-class function pointers. Our model does not require any complex domain-theoretical construction, instead, it is based on a novel step-indexed, direct-style operational semantics for our assembly language. From the model, we derive a new program logic named ISCAP (or Indexed SCAP). We use an example to demonstrate the power and simplicity of ISCAP. The semantic model, the ISCAP logic, and the soundness proofs have been implemented in the Coq proof assistant. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1109/TASE.2011.16 | TASE |
Keywords | Field | DocType |
semantic model,function pointers,first-class function pointers,simple model,iscap,high level languages,simple semantic model,certifying assembly programs,assembly program,assembly language,low-level assembly language,program logic,continuation passing style reasoning,function pointer,first-class function pointer,assembly code,first class function pointers,logic programming,certifying assembly program,assembly program certification,high-level languages,virtual function,indexation,assembly,cascading style sheets,registers,cognition,semantics,indexes | Pointer (computer programming),Operational semantics,Programming language,Function pointer,First-class function,Computer science,Correctness,Theoretical computer science,High-level programming language,Soundness,Proof assistant | Conference |
ISBN | Citations | PageRank |
978-1-4577-1487-0 | 2 | 0.38 |
References | Authors | |
14 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wei Wang | 1 | 257 | 34.45 |
| Zhong Shao | 2 | 897 | 68.80 |
| Xinyu Jiang | 3 | 8 | 8.27 |
| Yu Guo | 4 | 2 | 0.38 |