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 条
  • [31] Towards a Compiler for Reals
    Darulova, Eva
    Kuncak, Viktor
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2017, 39 (02):
  • [32] Securing a compiler transformation
    Deng, Chaoqiang
    Namjoshi, Kedar S.
    FORMAL METHODS IN SYSTEM DESIGN, 2018, 53 (02) : 166 - 188
  • [33] Formal certification of a compiler back-end or:: Programming a compiler with a proof assistant
    Leroy, X
    ACM SIGPLAN NOTICES, 2006, 41 (01) : 42 - 54
  • [34] Securing a compiler transformation
    Chaoqiang Deng
    Kedar S. Namjoshi
    Formal Methods in System Design, 2018, 53 : 166 - 188
  • [35] Model checking for multiagent systems: The MABLE language and its applications
    Wooldridge, M
    Huget, MP
    Fisher, M
    Parsons, S
    INTERNATIONAL JOURNAL ON ARTIFICIAL INTELLIGENCE TOOLS, 2006, 15 (02) : 195 - 225
  • [36] A compiler-compiler for Codesign
    Carchiolo, V
    Malgeri, M
    Mangioni, G
    INTERNATIONAL CONFERENCE ON POLITICS AND INFORMATION SYSTEMS: TECHNOLOGIES AND APPLICATIONS, PROCEEDINGS, 2003, : 174 - 177
  • [37] A structural transformation from p-π\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\pi $$\end{document} to MSVL
    Ling Luo
    Zhenhua Duan
    Cong Tian
    Xiaobing Wang
    Journal of Combinatorial Optimization, 2015, 29 (1) : 308 - 329
  • [38] Experience Report: a Do-It-Yourself High-Assurance Compiler
    Pike, Lee
    Wegmann, Nis
    Niller, Sebastian
    Goodloe, Alwyn
    ACM SIGPLAN NOTICES, 2012, 47 (09) : 335 - 340
  • [39] STEROIDS for DOPed Applications: A Compiler for Automated Data-Oriented Programming
    Pewny, Jannik
    Koppe, Philipp
    Holz, Thorsten
    2019 4TH IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY (EUROS&P), 2019, : 111 - 126
  • [40] A time-predictable VLIW processor and its compiler support
    Yan, Jun
    Zhang, Wei
    REAL-TIME SYSTEMS, 2008, 38 (01) : 67 - 84
12345