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 条
  • [21] Rewriting logic semantics for systemC scheduler
    Boutekkouk, Fateh
    Bilavarn, Sebastien
    Auguin, Michel
    Benmohammed, Mohamed
    [J]. International Review on Computers and Software, 2009, 4 (02) : 192 - 204
  • [22] Modular rewriting semantics of programming languages
    Meseguer, J
    Braga, C
    [J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 364 - 378
  • [23] A Sound Semantics for a Similarity-Based Logic Programming Language
    Julian-Iranzo, Pascual
    Rubio-Manzano, Clemente
    [J]. ADVANCES IN COMPUTATIONAL INTELLIGENCE, IWANN 2011, PT II, 2011, 6692 : 421 - 428
  • [24] THE PROGRAM CHARACTERISTICS IN LOGIC PROGRAMMING LANGUAGE ESP
    YAMAMOTO, A
    MITSUI, M
    YOSHIDA, H
    YOKOTA, M
    NAKAJIMA, K
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1986, 221 : 204 - 213
  • [25] LOGIC PROGRAMMING AS HYPERGRAPH REWRITING
    CORRADINI, A
    ROSSI, F
    PARISIPRESICCE, F
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 493 : 275 - 295
  • [26] Coalgebraic logic programming: from Semantics to Implementation
    Komendantskaya, Ekaterina
    Power, John
    Schmidt, Martin
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2016, 26 (02) : 745 - 783
  • [27] A REWRITING SEMANTICS FOR PROGRAM DEPENDENCE GRAPHS
    SELKE, RP
    [J]. CONFERENCE RECORD OF THE SIXTEENTH ANNUAL ACM SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 1989, : 12 - 24
  • [28] A causal semantics for CCS via rewriting logic
    Degano, P
    Gadducci, F
    Priami, C
    [J]. THEORETICAL COMPUTER SCIENCE, 2002, 275 (1-2) : 259 - 282
  • [29] The rewriting logic semantics project: A progress report
    Meseguer, Jose
    Rosu, Grigore
    [J]. INFORMATION AND COMPUTATION, 2013, 231 : 38 - 69
  • [30] Software specification and verification in rewriting logic
    Meseguer, J
    [J]. MODELS, ALGEBRAS AND LOGIC OF ENGINEERING SOFTWARE, 2003, 191 : 133 - 193
12345