Analysis of dynamic message passing programs (Record no. 340549)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 02265ntm a22002297a 4500 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | AT-ISTA |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20190813090716.0 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 160531s2013 au ||||| m||| 00| 0 eng d |
| 040 ## - CATALOGING SOURCE | |
| Transcribing agency | IST |
| 100 ## - MAIN ENTRY--PERSONAL NAME | |
| Personal name | Zufferey, Damien |
| 9 (RLIN) | 2635 |
| 245 ## - TITLE STATEMENT | |
| Title | Analysis of dynamic message passing programs |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) | |
| Name of publisher, distributor, etc. | IST Austria |
| Date of publication, distribution, etc. | 2013 |
| 500 ## - GENERAL NOTE | |
| General note | Thesis |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 1 Introduction, motivation, and related work |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 2 Toward a forward analysis of depth-bounded systems: domain of limits |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 3 Bridging the gap between theory and practice: ideal abstraction |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 4 Implementation: Picasso |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 5 Extensions: termination of depth-bounded systems, dynamic package interfaces |
| 505 ## - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 6 Conclusion |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | Motivated by the analysis of highly dynamic message-passing systems, i.e. unbounded thread creation, mobility, etc. We present a framework for the analysis of depth-bounded systems. Depth-bounded systems are one of the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. Even though they are infinite state systems depth-bounded<br/>systems are well-structured, thus can be analyzed algorithmically. We give an interpretation of depth-bounded systems as graph-rewriting systems. This gives more flexibility and ease of use to apply depth-bounded systems to other type<br/>of systems like shared memory concurrency.<br/>First, we develop an adequate domain of limits for depth-bounded systems, a prerequisite for the effective representation of downward-closed sets. Downwardclosed sets are needed by forward saturation-based algorithms to represent potentially infinite sets of states. Then, we present an abstract interpretation framework to compute the covering set of well-structured transition systems. Because, in general, the covering set is not computable, our abstraction overapproximates the actual covering set. Our abstraction captures the essence of acceleration based-algorithms while giving up enough precision to ensure convergence. We have implemented the analysis in the Picasso tool and show that it<br/>is accurate in practice. Finally, we build some further analyses like termination using the covering set as starting point. |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Source of classification or shelving scheme | Dewey Decimal Classification |
| Withdrawn status | Lost status | Source of classification or shelving scheme | Damaged status | Not for loan | Home library | Current library | Date acquired | Total Checkouts | Full call number | Barcode | Date last seen | Price effective from | Koha item type |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Not Lost | Dewey Decimal Classification | Library | Library | 31/05/2016 | Quiet Room | AT-ISTA#001148 | 15/09/2025 | 31/05/2016 | Book |