A novel approach to verifying context free properties of programs

Nan Zhang; Zhenhua Duan; Cong Tian; Hongwei Du

doi:10.1016/j.tcs.2020.01.005

A novel approach to verifying context free properties of programs

Nan Zhang
, Zhenhua Duan^*
, Cong Tian
, Hongwei Du

^*Corresponding author for this work

Xidian University
Harbin Institute of Technology Shenzhen

Research output: Contribution to journal › Article › peer-review

Abstract

This paper proposes an approach to verifying context free properties of programs. In this approach, the system to be verified is modeled as a program m in Modeling, Simulation and Verification Language (MSVL), and the desired property is also specified by an MSVL program m^′. Then program m and formula ¬m^′ are interpreted by means of executing programs m and m^′. If an acceptable execution path is generated, a counterexample is found, otherwise the property is valid. To show how the proposed approach works, an example is given.

Original language	English
Pages (from-to)	519-530
Number of pages	12
Journal	Theoretical Computer Science
Volume	809
DOIs	https://doi.org/10.1016/j.tcs.2020.01.005
State	Published - 24 Feb 2020
Externally published	Yes

Keywords

Algorithm
Automata
Model Checking
Runtime Verification
Temporal Logic

Access to Document

10.1016/j.tcs.2020.01.005

Cite this

@article{2116fe532bc34e9ea4e71a2122dbf7ad,

title = "A novel approach to verifying context free properties of programs",

abstract = "This paper proposes an approach to verifying context free properties of programs. In this approach, the system to be verified is modeled as a program m in Modeling, Simulation and Verification Language (MSVL), and the desired property is also specified by an MSVL program m′. Then program m and formula ¬m′ are interpreted by means of executing programs m and m′. If an acceptable execution path is generated, a counterexample is found, otherwise the property is valid. To show how the proposed approach works, an example is given.",

keywords = "Algorithm, Automata, Model Checking, Runtime Verification, Temporal Logic",

author = "Nan Zhang and Zhenhua Duan and Cong Tian and Hongwei Du",

note = "Publisher Copyright: {\textcopyright} 2020 Elsevier B.V.",

year = "2020",

month = feb,

day = "24",

doi = "10.1016/j.tcs.2020.01.005",

language = "英语",

volume = "809",

pages = "519--530",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - A novel approach to verifying context free properties of programs

AU - Zhang, Nan

AU - Duan, Zhenhua

AU - Tian, Cong

AU - Du, Hongwei

PY - 2020/2/24

Y1 - 2020/2/24

N2 - This paper proposes an approach to verifying context free properties of programs. In this approach, the system to be verified is modeled as a program m in Modeling, Simulation and Verification Language (MSVL), and the desired property is also specified by an MSVL program m′. Then program m and formula ¬m′ are interpreted by means of executing programs m and m′. If an acceptable execution path is generated, a counterexample is found, otherwise the property is valid. To show how the proposed approach works, an example is given.

AB - This paper proposes an approach to verifying context free properties of programs. In this approach, the system to be verified is modeled as a program m in Modeling, Simulation and Verification Language (MSVL), and the desired property is also specified by an MSVL program m′. Then program m and formula ¬m′ are interpreted by means of executing programs m and m′. If an acceptable execution path is generated, a counterexample is found, otherwise the property is valid. To show how the proposed approach works, an example is given.

KW - Algorithm

KW - Automata

KW - Model Checking

KW - Runtime Verification

KW - Temporal Logic

UR - https://www.scopus.com/pages/publications/85078043889

U2 - 10.1016/j.tcs.2020.01.005

DO - 10.1016/j.tcs.2020.01.005

M3 - 文章

AN - SCOPUS:85078043889

SN - 0304-3975

VL - 809

SP - 519

EP - 530

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

A novel approach to verifying context free properties of programs

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this