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 条
  • [21] Linear time-dependent constraints programming with MSVL
    Ma, Qian
    Duan, Zhenhua
    JOURNAL OF COMBINATORIAL OPTIMIZATION, 2014, 27 (04) : 724 - 766
  • [22] Implementation of Matlab matfun Toolkit Based on MSVL
    Feng, Xueqing
    Zhang, Nan
    Duan, Zhenhua
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2022, 2023, 13854 : 53 - 58
  • [23] Embedded Compiler Optimization for Communication Applications
    Lee, Jong-Yeol
    Yang, Won-Yong
    PROCEEDINGS OF THE 2010 IEEE ASIA PACIFIC CONFERENCE ON CIRCUIT AND SYSTEM (APCCAS), 2010, : 520 - 523
  • [24] Linear time-dependent constraints programming with MSVL
    Qian Ma
    Zhenhua Duan
    Journal of Combinatorial Optimization, 2014, 27 : 724 - 766
  • [25] A Proof System for MSVL Programs in Coq
    Qian, Lin
    Duan, Zhenhua
    Zhang, Nan
    Tian, Cong
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, 2017, 10189 : 121 - 143
  • [26] Model checking concurrent systems with MSVL
    Zhang, Nan
    Duan, Zhenhua
    Tian, Cong
    SCIENCE CHINA-INFORMATION SCIENCES, 2016, 59 (11)
  • [27] Translation Validation of Information Leakage of Compiler Optimizations
    Panigrahi, Priyanka
    Karfa, Chandan
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2023, 42 (11) : 3585 - 3598
  • [28] MSVL: a typed language for temporal logic programming
    Xiaobing Wang
    Cong Tian
    Zhenhua Duan
    Liang Zhao
    Frontiers of Computer Science, 2017, 11 : 762 - 785
  • [29] A Dataflow Programming Language and Its Compiler for Streaming Systems
    Wei, Haitao
    Zuckerman, Stephane
    Li, Xiaoming
    Gao, Guang R.
    2014 INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE, 2014, 29 : 1289 - 1298
  • [30] Object Pascal compiler for rapid development of Palm OS applications
    Ciocarlie, Horia
    Atanasoae, Marcela-Simona
    Ciocarlie, Mihai
    EUROCON 2007: THE INTERNATIONAL CONFERENCE ON COMPUTER AS A TOOL, VOLS 1-6, 2007, : 2534 - 2538
12345