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.
