Skip to main navigation Skip to search Skip to main content

A novel approach to verifying context free properties of programs

  • Nan Zhang
  • , Zhenhua Duan*
  • , Cong Tian
  • , Hongwei Du
  • *Corresponding author for this work
  • State Key Laboratory of Integrated Services Networks
  • Harbin Institute of Technology Shenzhen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

This paper proposes an approach to verifying programs against context free properties. To this end, the system to be verified is modeled by 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 languageEnglish
Title of host publicationAlgorithmic Aspects in Information and Management - 12th International Conference, AAIM 2018, Proceedings
EditorsSergiy Butenko, Shaojie Tang, Ding-Zhu Du, David Woodruff
PublisherSpringer Verlag
Pages74-87
Number of pages14
ISBN (Print)9783030046170
DOIs
StatePublished - 2018
Externally publishedYes
Event12th International Conference on Algorithmic Aspects in Information and Management, AAIM 2018 - Dallas, United States
Duration: 3 Dec 20184 Dec 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11343 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Conference on Algorithmic Aspects in Information and Management, AAIM 2018
Country/TerritoryUnited States
CityDallas
Period3/12/184/12/18

Keywords

  • Automata
  • Model checking
  • Runtime verification
  • Temporal logic

Fingerprint

Dive into the research topics of 'A novel approach to verifying context free properties of programs'. Together they form a unique fingerprint.

Cite this