Control and data abstraction: the cornerstones of practical formal verification
Y. Kesten, and A. Pnueli. 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.
Description
Control and data abstraction: the cornerstones of practical formal verification
%0 Journal Article
%1 yonit2000control
%A Kesten, Yonit
%A Pnueli, Amir
%D 2000
%J International Journal on Software Tools for Technology Transfer (STTT)
%K abstraction modelchecking networkinvariant parameterized verification
%N 4
%P 328--342
%T Control and data abstraction: the cornerstones of practical formal verification
%U http://dx.doi.org/10.1007/s100090050040
%V 2
%X 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.
@article{yonit2000control,
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.},
added-at = {2010-01-28T17:02:44.000+0100},
author = {Kesten, Yonit and Pnueli, Amir},
biburl = {https://www.bibsonomy.org/bibtex/21ccc3dad7da0770c8c3276a8f6289c13/giuliano.losa},
description = {Control and data abstraction: the cornerstones of practical formal verification},
interhash = {a091224ea74f293de6c09d5c476739c9},
intrahash = {1ccc3dad7da0770c8c3276a8f6289c13},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
keywords = {abstraction modelchecking networkinvariant parameterized verification},
month = mar,
number = 4,
pages = {328--342},
timestamp = {2010-01-28T17:02:44.000+0100},
title = {Control and data abstraction: the cornerstones of practical formal verification},
url = {http://dx.doi.org/10.1007/s100090050040},
volume = 2,
year = 2000
}