The Library
Assume-guarantee software verification based on game semantics
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, China, 01-03 Nov 2006. Published in: Formal Methods and Software Engineering, Proceedings, Volume 4260 pp. 529-548. ISBN 3-540-47460-9. ISSN 0302-9743.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
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 (Paper) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
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 | ||||
Official Date: | 2006 | ||||
Dates: |
|
||||
Volume: | Volume 4260 | ||||
Number of Pages: | 20 | ||||
Page Range: | pp. 529-548 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Conference Paper Type: | Paper | ||||
Title of Event: | 8th International Conference on Formal Engineering Methods (ICFEM 2006) | ||||
Type of Event: | Conference | ||||
Location of Event: | Macao, China | ||||
Date(s) of Event: | 01-03 Nov 2006 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |