西安电子科技大学学报（自然科学版）Issue(1)：75-81,7.DOI:10.3969/j.issn.1001-2400.2016.01.014
MSVL程序的自动定理证明方法
Automatic theorem proving technique for MSVL
摘要
Abstract
The MSVL is a temporal logic programming language . It can be used to verify C , Verilog/VHDL programs . To do so , a program written in C or Verilog/VHDL is translated to an MSVL program , and then the task is changed to verify MSVL programs . However , at present , the correctness of MSVL programs can only be proved by hand with deductive approaches . This is tedious and error-prone . To handle this problem , an automatic theorem proving technique for the MSVL based on the interactive theorem prover PVS is proposed . To this end , first the syntax and semantics of the MSVL are described in the specification language of PVS , which enables MSVL programs to be correctly recognized by PVS . Further , an axiomatic system of the MSVL and some theorems are specified . Then the proof commands of PVS are input for invoking the PVS prover to deduce MSVL programs . During verification , simple details can be proved by PVS automatically while complex steps are controlled by human . In this way , MSVL programs can be verified semi-automatically , which facilitates the deduction of MSVL programs . An instance of the bakery algorithm is given to show that our method is feasible .关键词
时序逻辑/公理系统/定理证明/验证Key words
temporal logic/axiomatic system/theorem proving/verification分类
信息技术与安全科学引用本文复制引用
马倩,段振华..MSVL程序的自动定理证明方法[J].西安电子科技大学学报（自然科学版）,2016,(1):75-81,7.基金项目
国家自然科学基金资助项目 （）
