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 条

[41] Provably correct edgel linking and subpixel boundary reconstruction
Koethe, Ullrich
Stelldinger, Peer
Meine, Hans
PATTERN RECOGNITION, PROCEEDINGS, 2006, 4174 : 81 - 90
[42] Provably correct hardware compilation using timing diagrams
Schenke, M
Dossis, M
FORMAL METHODS FOR PROTOCOL ENGINEERING AND DISTRIBUTED SYSTEMS, 1999, 28 : 313 - 331
[43] Designing provably correct information networks with digital diodes
Cohen, Fred
Computers and Security, 1988, 7 (03): : 279 - 286
[44] Synthesis of Provably Correct Autonomy Protocols for Shared Control
Cubuktepe, Murat
Jansen, Nils
Alshiekh, Mohammed
Topcu, Ufuk
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2021, 66 (07) : 3251 - 3258
[45] A Control Architecture for Provably-Correct Autonomous Driving
Aasi, Erfan
Vasile, Cristian Ioan
Belta, Calin
2021 AMERICAN CONTROL CONFERENCE (ACC), 2021, : 2913 - 2918
[46] Provably-Correct and Comfortable Adaptive Cruise Control
Althoff, Matthias
Maierhofer, Sebastian
Pek, Christian
IEEE TRANSACTIONS ON INTELLIGENT VEHICLES, 2021, 6 (01): : 159 - 174
[47] Provably Correct Smart Contracts: An Approach using DeepSEA
Britten, Daniel
Sjoberg, Vilhelm
Reeves, Steve
COMPANION PROCEEDINGS OF THE 2022 ACM SIGPLAN INTERNATIONAL CONFERENCE ON SYSTEMS, PROGRAMMING, LANGUAGES, AND APPLICATIONS: SOFTWARE FOR HUMANITY, SPLASH COMPANION 2022, 2022, : 5 - 6
[48] Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation
Liu, Jiawei
Xia, Chunqiu Steven
Wang, Yuyao
Zhang, Lingming
ADVANCES IN NEURAL INFORMATION PROCESSING SYSTEMS 36 (NEURIPS 2023), 2023,
[49] AUTOMATED CODE GENERATION FOR SAFETY-RELATED APPLICATIONS: A CASE STUDY
Gluch, David P.
Kornecki, Andrew J.
COMPUTER SCIENCE-AGH, 2007, 8 : 37 - 48
[50] PROVABLY GOOD MESH GENERATION
BERN, M
EPPSTEIN, D
GILBERT, J
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1994, 48 (03) : 384 - 409

← 1 2 3 4 5 →