Analysis of dynamic message passing programs (Record no. 340549)

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
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
of systems like shared memory concurrency.
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
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
Holdings
Withdrawn status Lost status Source of classification or shelving scheme Damaged status Not for loan Permanent Location Current Location Date acquired Barcode Date last seen Price effective from Koha item type
  Not Lost       Library Library 2016-05-31 AT-ISTA#001148 2018-11-06 2016-05-31 Book

Powered by Koha