A compiler for MSVL and its applications

被引：19
|
作者：
Yang, Kai
Duan, Zhenhua [1 ]
Tian, Cong [1 ]
Zhang, Nan
机构：
[1] Xidian Univ, ICTT, Xian 710071, Shaanxi, Peoples R China
来源：
THEORETICAL COMPUTER SCIENCE | 2018年 / 749卷
基金：
中国国家自然科学基金;
关键词：
MSVL; Model checking; Compiler; Verification; Al planning; DYNAMIC THERMAL MANAGEMENT; TEMPORAL LOGIC; VERIFICATION;
D O I：
10.1016/j.tcs.2017.07.032
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper, we present a method for implementing a compiler called MC for Modeling, Simulation and Verification Language (MSVL) based on LLVM. MC accepts a well formed MSVL program as input and generates an executable binary code. Different from other compilers, MC can be used not only to compile programs but also to model and verify programs. The details of implementation including the architecture design, lexical, syntactic and semantic analysis, as well as preprocessing and scheduling algorithms. Besides, we show MC can be utilized as an infrastructure for Artificial Intelligence (Al) planning. Several examples are given to show applications of MC in modeling and verifying programs, as well as Al planning. (C) 2017 Elsevier B.V. All rights reserved.
引用
收藏
页码：2 / 16
页数：15
相关论文
共 50 条
  • [41] A time-predictable VLIW processor and its compiler support
    Jun Yan
    Wei Zhang
    Real-Time Systems, 2008, 38 : 67 - 84
  • [42] A Formally Verified Compiler for Lustre
    Bourke, Timothy
    Brun, Lelio
    Dagand, Pierre-Evariste
    Leroy, Xavier
    Pouzet, Marc
    Rieg, Lionel
    ACM SIGPLAN NOTICES, 2017, 52 (06) : 586 - 601
  • [43] Insertion Modeling and Its Applications
    Letichevsky, Alexander
    Letychevskyi, Oleksandr
    Peschanenko, Vladimir
    COMPUTER SCIENCE JOURNAL OF MOLDOVA, 2016, 24 (03) : 357 - 370
  • [44] A Verified Compiler for an Impure Functional Language
    Chlipala, Adam
    ACM SIGPLAN NOTICES, 2010, 45 (01) : 93 - 106
  • [45] A High Speed Signal Processing Machine -Its Architecture, Language and Compiler
    Wang Yufei and Yu ShiqiBeijing Institute of Data Processing Technology
    Journal of Systems Engineering and Electronics, 1991, (01) : 119 - 128
  • [46] Automatically proving the correctness of compiler optimizations
    Lerner, S
    Millstein, T
    Chambers, C
    ACM SIGPLAN NOTICES, 2003, 38 (05) : 220 - 231
  • [47] AXIOMATIC BOOTSTRAPPING - A GUIDE FOR COMPILER HACKERS
    APPEL, AW
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (06): : 1699 - 1718
  • [48] TEMPORAL LOGIC AND APPLICATIONS - A TUTORIAL
    GOTZHEIN, R
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1992, 24 (03): : 203 - 218
  • [49] A type-preserving compiler in Haskell
    Guillemette, Louis-Julien
    Monnier, Stefan
    ACM SIGPLAN NOTICES, 2008, 43 (09) : 75 - 86
  • [50] Computational logic: its origins and applications
    Paulson, Lawrence C.
    PROCEEDINGS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2018, 474 (2210):
12345