Title :
Making PVS do what you want
Author_Institution :
Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
Abstract :
We focus on how to capture common specification and proof patterns in PVS in order to tailor PVS for the verification of a particular class of systems. The use of specification templates can simplify the development of PVS strategies that correspond to proof steps that recur in proofs of specific classes of system properties.
Keywords :
formal specification; formal verification; PVS strategy; formal specification; formal verification; proof patterns;
Conference_Titel :
Formal Methods and Models for Co-Design, 2005. MEMOCODE '05. Proceedings. Third ACM and IEEE International Conference on
Print_ISBN :
0-7803-9227-2
DOI :
10.1109/MEMCOD.2005.1487893
