Sciweavers

CAV
1998
Springer

You Assume, We Guarantee: Methodology and Case Studies

14 years 4 months ago
You Assume, We Guarantee: Methodology and Case Studies
Assume-guarantee reasoning has long been advertised as an important method for decomposing proof obligations in system veri cation. Re nement mappings (homomorphisms) have long been advertised as an important method for solving the language-inclusion problem in practice. When confronted with large veri cation problems, we therefore attempted to make use of both techniques. We soon found that rather than o ering instant solutions, the success of assumee reasoning depends critically on the construction of suitable abstraction modules, and the success of re nement checking depends critically on the construcsuitable witness modules. Moreover, as abstractions need to be witnessed, esses abstracted, the process must be iterated. We present here the main lessons we learned from our experiments, in form of a systematic and structured discipline for the compositional veri cation of reactive modules. An infrastructure to support this discipline, and automate parts of the veri cation, has been im...
Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajama
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where CAV
Authors Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani
Comments (0)