The Library
Assume-guarantee software verification based on game semantics
Tools
Tools
Tools
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.Abstract
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 |
| Publisher: | SPRINGER-VERLAG BERLIN |
| ISBN: | 3-540-47460-9 |
| ISSN: | 0302-9743 |
| Editor: | Liu, Z and He, J |
| Date: | 2006 |
| Volume: | 4260 |
| Number of Pages: | 20 |
| Page Range: | pp. 529-548 |
| Publication Status: | Published |
| 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 |
| URI: | http://wrap.warwick.ac.uk/id/eprint/30953 |
Data sourced from Thomson Reuters' Web of Knowledge
Actions (login required)
 |
View Item |
