Article,

Control and data abstraction: the cornerstones of practical formal verification

, and .
International Journal on Software Tools for Technology Transfer (STTT), 2 (4): 328--342 (March 2000)

Abstract

Abstract.   In spite of the impressive progress in the development of the two main methods for formal verification of reactive systems – Symbolic Model Checking and Deductive Verification, they are still limited in their ability to handle large systems. Itis generally recognized that the only way these methods can ever scale up is by the extensive use of abstraction and modularization,which break the task of verifying a large system into several smaller tasks of verifying simpler systems.

Tags

Users

  • @giuliano.losa

Comments and Reviews