PVS is a verification system: It consists of a specification language and a theorem prover. Using mechanized formal methods, theories are proven and verified. Maple is a computer algebra system: It is a tool for solving mathematical problems including symbolic computation. Employing specialized algorithms, mathematical problems are solved.
Because of the limitations of the system, Maple cannot guarantee correctness of all answers. PVS can guarantee correctness by providing formal proofs. To combine the strengths of Maple and PVS, it becomes necessary to enable Maple to access the functionalities of PVS. We archieve this objective by designing and implementing an interface between these two systems. Through this interface, a Maple user can access PVS from a Maple worksheet without knowing the underlying communication mechanisms between the systems.