中文摘要：

时序逻辑程序设计语言能被用于验证C、Verilog/VHDL程序的正确性.但目前时序逻辑程序设计语言程序只能纯手工进行定理证明.针对该问题提出了一种基于定理证明器原型验证系统的时序逻辑程序设计语言程序的自动定理证明方法.该方法首先使用原型验证系统规范语言描述时序逻辑程序设计语言的语法和语义,使得原型验证系统能够正确识别时序逻辑程序设计语言程序;然后使用原型验证系统规范语言描述时序逻辑程序设计语言的公理系统和待证定理;最后输入原型验证系统命令调用原型验证系统证明器来进行时序逻辑程序设计语言程序的推演证明.在证明过程中,细节被原型验证系统自动地证明,使得人工仅在复杂的步骤上指导控制,从而实现半自动地验证时序逻辑程序设计语言程序,简化了该定理的证明过程.

英文摘要：

The MSVL is a temporal logic programming language.It can be used to verify C,Verilog/VHDL programs.To do so,aprogram 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.