1,721,012 research outputs found
Resource bound analysis of imperative programs
Full text linkIn vielen praktischen Anwendungen benötigt man eine Beschränkung der von Computerprogrammen verbrauchten Resourcen (z.B. Ausführungszeit, Speicher, Netzwerkverkehr, Energie) und eine Abschätzung von quantitativen Programmeigenschaften (z.B. des Verlusts geheimer Informationen oder der Ausbreitung von Fehlern). Viele dieser Fragen lassen sich auf das Problem der Berechnung einer symbolischen Schranke zurückführen, wie oft ein bestimmter Programmpunkt in Abhängigkeit von den Programmeingaben besucht werden kann; wir nennen dies das Erreichbarkeitsschrankenproblem.Die in dieser Dissertation vorgestellte Methode berechnet eine Erreichbarkeitsschranke eines gegebenen Programmpunktes in zwei Schritten:Im ersten Schritt erzeugen wir ein Transitionssystem, das disjunktiv alle Paare von Zuständen zusammenfasst, für die es eine Programmausführung gibt, die den Programmpunkt mindestens zweimal besucht. Im zweiten Schritt berechnen wir eine Schranke für das Transitionssystem. Wir präsentieren zwei Ansätze, die unsere Methode praktisch umsetzen.Unser erster Ansatz verwendet eine auf abstrakter Interpretation basierende iterative Technik zur Berechnung disjunktiver Schleifeninvarianten und eine nicht-iterative auf Beweisregeln basierende Technik für die Berechnung von Schranken. Wir evaluieren die Effizienz unseres Ansatzes an einer .Net Bibliothek und weiteren Benchmark Programmen.Unser zweiter Ansatz basiert auf der sogenannten size-change Abstraktion (SCA), die das monotone Verhalten numerischer Größen über den Programmzuständen beschreibt. Wir nützen eine Abschlusseigenschaft von SCA zur Berechnung disjunktiver Schleifeninvarianten. Mit Hilfe von SCA können wir Schranken stufenweise berechnen: Zunächst extrahieren wir lokale Fortschrittsmaße aus kleinen Programmabschnitten und setzen diese dann zu einer global gültigen Schranke zusammen. Durch zwei geeignete Programmtransformationen ermöglichen wir die Schrankenanalyse imperativer Programme. Wir evaluieren die Effizienz unserer Ansatzes anhand zweier Benchmarks für die Sprache C.Im Anschluss präsentieren wir theoretische Beiträge, die auf eine mathematische Charakterisierung jener Schranken, die mit SCA ausgedrückt werden können, hinarbeiten. Zusammenfassend diskutieren wir, wie unser Lösungsansatz des Erreichbarkeitsschrankenproblems auf den wesentlichen Ideen früherer Terminations- und Schleifenanalysen aufbaut und diese verbessert.For many practical applications it is important to bound the resources consumed by a program such as time, memory, network-traffic, power, and to estimate quantitative properties of data in programs, such as information leakage or uncertainty propagation. At the heart of many of these questions lies the problem of finding a symbolic worst-case bound on the number of visits to a given program location in terms of the inputs to that program; we call this the reachability-bound problem.We propose a two-step methodology for computing a reachability-bound of a given program location: First, we generate a transition system that disjunctively summarizes all pairs of states for which there is a program execution that visits the location once and again. Second, we compute a bound of the transition system. We present two approaches that implement this methodology.Our first approach brings together an abstract-interpretation based iterative technique for computing disjunctive loop invariants and a non-iterative proof-rules based technique for loop bound computation. We evaluate the effectiveness of this approach on a .Net base-class library and further benchmark programs.Our second approach is based on the so-called size-change abstraction (SCA). We use a closure property of SCA for computing disjunctive loop invariants. We show that SCA offers a separation of concerns for bound computation: we extract local progress measures from small program parts, and then compose these local progress measures to a global bound.We state two program transformations that make imperative programs amenable to bound analysis with SCA. We evaluate the effectiveness of this approach on two C benchmarks.We further present results towards a theoretical characterization of the bounds expressible by SCA.Finally we show that our solution to the reachability-bound problem captures the essential ideas of earlier termination and bound analyses and goes beyond in a simpler framework.<br /
A Framework for Mass-Market Inductive Program Synthesis
No full textThesis (Ph.D.)--University of Washington, 2017-06Programming by examples (PBE), or inductive program synthesis, is a problem of finding a program in the underlying domain-specific language (DSL) that is consistent with the given input-output examples or constraints. In the last decade, it has gained a lot of prominence thanks to the mass-market deployments of several PBE-based technologies for data wrangling – the widespread problem of transforming raw datasets into a structured form, more amenable to analysis. However, deployment of a mass-market application of program synthesis is challenging. First, an efficient implementation requires non-trivial engineering insight, often overlooked in a research prototype. This insight takes the form of domain-specific knowledge and heuristics, which complicate the implementation, extensibility, and maintenance of the underlying synthesis algorithm. Second, application development should be fast and agile, tailoring to versatile market requirements. Third, the underlying synthesis algorithm should be accessible to the engineers responsible for product maintenance. In this work, I show how to generalize the ideas of 10 + previous specialized inductive synthesizers into a single framework, which facilitates automatic generation of a domain-specific synthesizer from the mere definition of the corresponding DSL and its properties. PROSE (PROgram Synthesis using Examples) is the first program synthesis framework that explicitly separates domain-agnostic search algorithms from domain-specific expert insight, making the resulting synthesizer both fast and accessible. The underlying synthesis algorithm pioneers the use of deductive reasoning for designer-defined domain-specific operators and languages, which enables mean synthesis times of 1-3 sec on real-life datasets. A dedicated team at Microsoft has built and deployed 10 + technologies on top of the PROSE framework. Using them as case studies, I examine the user interaction challenges that arise after a mass-market deployment of a PBE-powered application. I show how expressing program synthesis as an interactive problem facilitates user intent disambiguation, incremental learning from additional examples, and increases the users’ confidence in the system
Learning-based inductive invariant synthesis
Full text linkThe problem of synthesizing adequate inductive invariants to prove a program correct lies at the heart of automated program verification. We investigate, herein, learning approaches to synthesize inductive invariants of sequential programs towards automatically verifying them. To this end, we identify that prior learning approaches were unduly influenced by traditional machine learning models that learned concepts from positive and negative counterexamples. We argue that these models are not robust for invariant synthesis and, consequently, introduce ICE, a robust learning paradigm for synthesizing invariants that learns using positive, negative and implication counterexamples, and show that it admits honest teachers and strongly convergent mechanisms for invariant synthesis. We develop the first learning algorithms in this model with implication counterexamples for two domains, one for learning arbitrary Boolean combinations of numerical invariants over scalar variables and one for quantified invariants of linear data-structures including arrays and dynamic lists. We implement the ICE learners and an appropriate teacher, and show that the resulting invariant synthesis is robust, practical, convergent, and efficient.
In order to deductively verify shared-memory concurrent programs, we present a sequentialization result and show that synthesizing rely-guarantee annotations for them can be reduced to invariant synthesis for sequential programs. Further, for verifying asynchronous event-driven systems, we develop a new invariant synthesis technique that constructs almost-synchronous invariants over concrete system configurations. These invariants, for most systems, are finitely representable, and can be thereby constructed, including for the USB driver that ships with Microsoft Windows phone.Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2015-09-29 without embargo termsThe student, Pranav Garg, accepted the attached license on 2015-07-13 at 10:16.The student, Pranav Garg, submitted this Dissertation for approval on 2015-07-13 at 10:31.This Dissertation was approved for publication on 2015-07-14 at 11:41.DSpace SAF Submission Ingestion Package generated from Vireo submission #8418 on 2015-09-29 at 13:22:39Made available in DSpace on 2015-09-29T20:38:20Z (GMT). No. of bitstreams: 2
GARG-DISSERTATION-2015.pdf: 2048698 bytes, checksum: f2a9aaeb832ba2aca78a182f4577f2bc (MD5)
LICENSE.txt: 4208 bytes, checksum: 6d4b5511fa73374fd27e44f807d4b1d6 (MD5)
Previous issue date: 2015-07-1
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Verification of linear-time properties for finite probabilistic systems
Full text linkWith computers becoming ubiquitous there is an ever growing necessity to ensure that they are programmed to behave correctly. Formal verification is a discipline within computer science that tackles issues related to design and analysis of programs with the aim of producing well behaved systems. One of the core problems in this domain is what is called the model checking problem: given a mathematical model of a computer and a correctness specification, does the model satisfy the specification? In this thesis we explore this question for Markov Decision Processes (MDPs), which are finite state models involving stochastic and non-deterministic behaviour over discrete time steps. The kind of specifications we focus on are those that describe the correctness of individual executions of the model, called linear time properties. We delve into two different semantics for assigning meaning to the model checking problem: execution based semantics and distribution based semantics.
In the execution based semantics we look at specifications described using Linear Temporal Logic (LTL). The model checking problem under this semantics are of two kinds: qualitative and quantitative. In the qualitative version we are interested in finding out if the specification is satisfied with non-zero probability, and in the more general quantitative version we want to know whether the probability of satisfaction is greater than a given quantity. The standard way to do model checking for both cases involves translating the LTL formula into an automaton which is then used to analyze the given MDP. One of the contributions of this thesis is a new translation of LTL to automata that are provably smaller than previously known ones. This translation helps us in reducing the asymptotic complexity of qualitative model checking of MDPs against certain fragments of LTL. We implement this translation in a tool called Büchifier to show its benefits on real examples. Our second main contribution involves a new automata-based algorithm for quantitative model checking that along with known translations of LTL to automata, which gives us new complexity results for the problem for different fragments of LTL.
In the distribution based semantics we view MDPs as producing a sequence of probability distributions over its state space. At each point of time we are interested in the truth of atomic propositions, each of which tells us whether the probability of being in a certain states is above or below a given threshold. Linear time properties over these propositions are then used to describe correctness criteria. The model checking problem here happens to be undecidable in general, and therefore we consider restrictions on the problem. First we consider propositions which are robust: a proposition is said to be robust when the probability of being in its associated set of states is always well separated from its given threshold. For properties described over such propositions we observe that the model checking problem becomes decidable. But checking for robustness itself is an undecidable problem for MDPs. So we focus our attention on a subclass of MDPs called Markov Chains which exhibit stochastic behaviour without non-determinism. For Markov Chains we show that checking for robustness and model checking under robustness become tractable and we provide an analysis of the computational complexity of these problems.Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-03-13 without embargo termsThe student, Dileep Kini, accepted the attached license on 2017-12-02 at 09:39.The student, Dileep Kini, submitted this Dissertation for approval on 2017-12-02 at 09:41.This Dissertation was approved for publication on 2017-12-05 at 08:36.DSpace SAF Submission Ingestion Package generated from Vireo submission #11811 on 2018-03-13 at 10:09:50Made available in DSpace on 2018-03-13T15:48:50Z (GMT). No. of bitstreams: 5
KINI-DISSERTATION-2017.pdf: 2066486 bytes, checksum: b2964e6d5edbc78a70f74e258cfa4b0f (MD5)
Thesis-Title.pdf: 84468 bytes, checksum: 202621997446661452f02e248ab5a8e7 (MD5)
Thesis.zip: 2193798 bytes, checksum: b185a0f48e96dd202369451fe0306e32 (MD5)
LICENSE.txt: 4208 bytes, checksum: 7e2a788bff14536086f6df4a1f5fb3ab (MD5)
PROQUEST_LICENSE.txt: 4554 bytes, checksum: f8fca03cdccb6a62e25d92aad10f8259 (MD5)
Previous issue date: 2017-12-0
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Appropriate Similarity Measures for Author Cocitation Analysis
Full text linkWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
Dispelling the Myths Behind First-author Citation Counts
Full text linkWe conducted a full-scale evaluative citation analysis study of scholars in the XML research field to explore just how different from each other author rankings resulting from different citation counting methods actually are, and to demonstrate the capability of emerging data and tools on the Web in supporting more realistic citation counting methods. Our results contest some common arguments for the continued
use of first-author citation counts in the evaluation of scholars, such as high correlations between author rankings by first-author citation counts and other citation
counting methods, and high costs of using more realistic citation counting methods that are not well-supported by the ISI databases. It is argued that increasingly available digital full text research papers make it possible for citation analysis studies to go beyond what the ISI databases have directly supported and to employ more
sophisticated methods
- …
