Algorithmic advances in program analysis and their applications (Record no. 373534)

000 -LEADER
fixed length control field 06164nam a22003617a 4500
003 - CONTROL NUMBER IDENTIFIER
control field AT-ISTA
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20190813092332.0
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 180627b xxu||||| |||| 00| 0 eng d
040 ## - CATALOGING SOURCE
Transcribing agency IST
100 ## - MAIN ENTRY--PERSONAL NAME
Personal name Pavlogiannis, Andreas
9 (RLIN) 4262
245 ## - TITLE STATEMENT
Title Algorithmic advances in program analysis and their applications
260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Name of publisher, distributor, etc. IST Austria
Date of publication, distribution, etc. 2017
500 ## - GENERAL NOTE
General note Thesis
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note Acknowledgments<br/>
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note Abstract
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note List of Tables
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note List of Figures
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note List of Abbreviations
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 1 Introduction
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 2 Preliminaries
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 3 Semiring Distance Oracles on Low-treewidth Graphs
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 4 Semiring Distance on RSMs of Constant Treewidth
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 5 Optimal Dyck Reachability with Applications to Data-dependence and Alias Analysis
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 6 Quantitative Interprocedural Analysis
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 7 Semiring Distances on Concurrent Systems of Constant-treewidth Components
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 8 Quantitative Verification on Constant-treewidth Graphs
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 9 Data-centric Dynamic PArtial Order Reduction
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note 10 Automated Competitive Analysis in Real-time Scheduling with Graphs and Games
505 ## - FORMATTED CONTENTS NOTE
Formatted contents note Bibliography
520 ## - SUMMARY, ETC.
Summary, etc. This dissertation focuses on algorithmic aspects of program verification, and presents modeling and complexity advances on several problems related to the<br/> static analysis of programs, the stateless model checking of concurrent programs, and the competitive analysis of real-time scheduling algorithms.<br/> Our contributions can be broadly grouped into five categories.<br/> <br/> Our first contribution is a set of new algorithms and data structures for the quantitative and data-flow analysis of programs, based on the graph-theoretic notion of treewidth.<br/> It has been observed that the control-flow graphs of typical programs have special structure, and are characterized as graphs of small treewidth.<br/> We utilize this structural property to provide faster algorithms for the quantitative and data-flow analysis of recursive and concurrent programs.<br/> In most cases we make an algebraic treatment of the considered problem,<br/> where several interesting analyses, such as the reachability, shortest path, and certain kind of data-flow analysis problems follow as special cases. <br/> We exploit the constant-treewidth property to obtain algorithmic improvements for on-demand versions of the problems, <br/> and provide data structures with various tradeoffs between the resources spent in the preprocessing and querying phase.<br/> We also improve on the algorithmic complexity of quantitative problems outside the algebraic path framework,<br/> namely of the minimum mean-payoff, minimum ratio, and minimum initial credit for energy problems.<br/> <br/> <br/> Our second contribution is a set of algorithms for Dyck reachability with applications to data-dependence analysis and alias analysis.<br/> In particular, we develop an optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous in context-insensitive, field-sensitive points-to analysis.<br/> Additionally, we develop an efficient algorithm for context-sensitive data-dependence analysis via Dyck reachability,<br/> where the task is to obtain analysis summaries of library code in the presence of callbacks.<br/> Our algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is (i)~linear in the number of call sites and (ii)~only logarithmic in the size of the whole library, as opposed to linear in the size of the whole library.<br/> Finally, we prove that Dyck reachability is Boolean Matrix Multiplication-hard in general, and the hardness also holds for graphs of constant treewidth.<br/> This hardness result strongly indicates that there exist no combinatorial algorithms for Dyck reachability with truly subcubic complexity.<br/> <br/> <br/> Our third contribution is the formalization and algorithmic treatment of the Quantitative Interprocedural Analysis framework.<br/> In this framework, the transitions of a recursive program are annotated as good, bad or neutral, and receive a weight which measures<br/> the magnitude of their respective effect.<br/> The Quantitative Interprocedural Analysis problem asks to determine whether there exists an infinite run of the program where the long-run ratio of the bad weights over the good weights is above a given threshold.<br/> We illustrate how several quantitative problems related to static analysis of recursive programs can be instantiated in this framework,<br/> and present some case studies to this direction.<br/> <br/> <br/> Our fourth contribution is a new dynamic partial-order reduction for the stateless model checking of concurrent programs. Traditional approaches rely on the standard Mazurkiewicz equivalence between traces, by means of partitioning the trace space into equivalence classes, and attempting to explore a few representatives from each class.<br/> We present a new dynamic partial-order reduction method called the Data-centric Partial Order Reduction (DC-DPOR).<br/> Our algorithm is based on a new equivalence between traces, called the observation equivalence.<br/> DC-DPOR explores a coarser partitioning of the trace space than any exploration method based on the standard Mazurkiewicz equivalence.<br/> Depending on the program, the new partitioning can be even exponentially coarser.<br/> Additionally, DC-DPOR spends only polynomial time in each explored class.<br/> <br/> <br/> Our fifth contribution is the use of automata and game-theoretic verification techniques in the competitive analysis and synthesis of real-time scheduling algorithms for firm-deadline tasks.<br/> On the analysis side, we leverage automata on infinite words to compute the competitive ratio of real-time schedulers subject to various environmental constraints.<br/> On the synthesis side, we introduce a new instance of two-player mean-payoff partial-information games, and show<br/> how the synthesis of an optimal real-time scheduler can be reduced to computing winning strategies in this new type of games.
856 ## - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://doi.org/10.15479/AT:ISTA:th_854">https://doi.org/10.15479/AT:ISTA:th_854</a>
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 2018-06-27 AT-ISTA#001524 2018-11-06 2018-06-27 Book

Powered by Koha