Assume-guarantee software verification based on game semantics
Dimovski, Aleksandar and Lazic, Ranko (2006) Assume-guarantee software verification based on game semantics. In: 8th International Conference on Formal Engineering Methods (ICFEM 2006), Macao, PEOPLES R CHINA, NOV 01-03, 2006. Published in: Formal Methods and Software Engineering, Proceedings, 4260 pp. 529-548.Full text not available from this repository.
We show how game semantics, counterexample-guided abstraction refinement, assume-guarantee reasoning and the L* algorithm for learning regular languages can be combined to yield a procedure for compositional verification of safety properties of open programs. Game semantics is used to construct accurate models of subprograms compositionally. Overall model construction is avoided using assume-guarantee reasoning and the L* algorithm, by learning assumptions for arbitrary subprograms. The procedure has been implemented, and initial experimental results show significant space savings.
|Item Type:||Conference Item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software|
|Series Name:||LECTURE NOTES IN COMPUTER SCIENCE|
|Journal or Publication Title:||Formal Methods and Software Engineering, Proceedings|
|Editor:||Liu, Z and He, J|
|Number of Pages:||20|
|Page Range:||pp. 529-548|
|Title of Event:||8th International Conference on Formal Engineering Methods (ICFEM 2006)|
|Location of Event:||Macao, PEOPLES R CHINA|
|Date(s) of Event:||NOV 01-03, 2006|
Actions (login required)