Provably Correct Code Generation: A Case Study

被引：2
|
作者：
Wang, Qian [1 ]
Gupta, Gopal [1 ]
机构：
[1] Univ Texas Dallas, Dept Comp Sci, Dallas, TX 75083 USA
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 118卷
关键词：
Horn logic; Denotational Semantics; Compilation;
D O I：
10.1016/j.entcs.2004.11.008
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we present an approach to provably correct compilation based on Horn logical semantics of programming languages and partial evaluation. We also show that continuation semantics can be expressed in the Horn logical framework, and introduce Definite Clause Semantics. We illustrate our approach by developing the semantics for the SCR specification language, and using it to (automatically) generate target code in a provably correct manner.
引用
收藏
页码：87 / 109
页数：23
相关论文
共 50 条
  • [1] Towards provably correct code generation via horn logical continuation semantics
    Wang, Q
    Gupta, G
    Leuschel, M
    [J]. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, PROCEEDINGS, 2005, 3350 : 98 - 112
  • [2] Automatic generation of provably correct parallelizing compilers
    Gupta, G
    Pontelli, E
    Lara-Rodriguez, A
    Felix-Cardenas, R
    [J]. 1998 INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING - PROCEEDINGS, 1998, : 579 - 586
  • [3] Towards semi-automatic generation of provably correct algorithmic programs
    Shi, Haihe
    Xue, Jinyun
    [J]. SNPD 2007: EIGHTH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING, AND PARALLEL/DISTRIBUTED COMPUTING, VOL 3, PROCEEDINGS, 2007, : 952 - +
  • [4] CORRECT AND PROVABLY EFFICIENT METHODS FOR RECTILINEAR STEINER SPANNING TREE GENERATION
    LEWIS, FD
    VANCLEAVE, N
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 507 : 329 - 335
  • [5] A PROVABLY CORRECT COMPILER GENERATOR
    PALSBERG, J
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 582 : 418 - 434
  • [6] Automatic Patch Generation by Learning Correct Code
    Long, Fan
    Rinard, Martin
    [J]. ACM SIGPLAN NOTICES, 2016, 51 (01) : 298 - 312
  • [7] Provably correct theories of action
    Univ of Toronto, Toronto, Canada
    [J]. J Assoc Comput Mach, 2 (293-320):
  • [8] PROVABLY CORRECT CRITICAL PATHS
    MCGEER, PC
    BRAYTON, RK
    [J]. ADVANCED RESEARCH IN VLSI : PROCEEDINGS OF THE DECENNIAL CALTECH CONFERENCE ON VLSI, 1989, : 119 - 142
  • [9] Provably correct runtime monitoring
    School of Computer Science and Communication, KTH, Sweden
    不详
    [J]. J. Logic. Algebraic Program., 1600, 5 (304-339):
  • [10] PROVABLY CORRECT THEORIES OF ACTION
    LIN, FZ
    SHOHAM, Y
    [J]. JOURNAL OF THE ASSOCIATION FOR COMPUTING MACHINERY, 1995, 42 (02): : 293 - 320
12345