From Rewriting Logic, to Programming Language Semantics, to Program Verification

被引：9
|
作者：
Rosu, Grigore [1 ]
机构：
[1] Univ Illinois, Champaign, IL 61801 USA
来源：
LOGIC, REWRITING, AND CONCURRENCY | 2015年 / 9200卷
关键词：
K SEMANTICS; P SYSTEMS;
D O I：
10.1007/978-3-319-23165-5_28
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Rewriting logic has proven to be an excellent formalism to define executable semantics of programming languages, concurrent or not, and then to derive formal analysis tools for the defined languages with very little effort, such as model checkers. In this paper we give an overview of recent results obtained in the context of the rewriting logic semantics framework K, such as complete semantics of large programming languages like C, Java, JavaScript, Python, and deductive program verification techniques that allow us to verify programs in these languages using a common verification infrastructure.
引用
收藏
页码：598 / 616
页数：19
相关论文
共 50 条
  • [1] Rewriting Logic Semantics and Verification of Model Transformations
    Boronat, Artur
    Heckel, Reiko
    Meseguer, Jose
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5503 : 18 - +
  • [2] Rewriting Logic Semantics of a Plan Execution Language
    Dowek, Gilles
    Munoz, Cesar
    Rocha, Camilo
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (18): : 77 - 91
  • [3] Rewriting logic semantics: From language specifications to formal analysis tools
    Meseguer, J
    Rosu, G
    [J]. AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 1 - 44
  • [4] SEMANTICS OF PREDICATE LOGIC AS A PROGRAMMING LANGUAGE
    VANEMDEN, MH
    KOWALSKI, RA
    [J]. JOURNAL OF THE ACM, 1976, 23 (04) : 733 - 742
  • [5] LOGIC PROGRAM SEMANTICS FOR PROGRAMMING WITH EQUATIONS
    JAFFAR, J
    STUCKEY, PJ
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1986, 225 : 313 - 326
  • [6] A REWRITING LOGIC SEMANTICS APPROACH TO MODULAR PROGRAM ANALYSIS
    Hills, Mark
    Rosu, Grigore
    [J]. PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'10), 2010, 6 : 151 - 160
  • [7] The Semantics of Dynamic Fuzzy Logic Programming Language
    Zhao, Xiaofang
    [J]. EMERGING RESEARCH IN ARTIFICIAL INTELLIGENCE AND COMPUTATIONAL INTELLIGENCE, 2011, 237 : 272 - 279
  • [8] A verification logic for rewriting logic
    Martí-Oliet, N
    Pita, I
    Fiadeiro, JL
    Meseguer, J
    Maibaum, T
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2005, 15 (03) : 317 - 352
  • [9] Formal verification of a programming logic for a distributed programming language
    Zhang, C
    Olsson, RA
    Levitt, KN
    [J]. THEORETICAL COMPUTER SCIENCE, 1999, 216 (1-2) : 213 - 235
  • [10] The rewriting logic semantics project
    Meseguer, Jose
    Rosu, Grigore
    [J]. THEORETICAL COMPUTER SCIENCE, 2007, 373 (03) : 213 - 237
12345