scholarly journals Abstract Interpretation over Zones without Widening

10.29007/qqdg ◽  
2018 ◽  
Author(s):  
Thomas Martin Gawlitza ◽  
Helmut Seidl
Keyword(s):  
Abstract Interpretation ◽  
Monotone Operators ◽  
Worst Case ◽  
Running Time ◽  
Practical Algorithm ◽  
Abstract Semantics

We present a practical algorithm for computing leastsolutions of systems of (fixpoint-)equations over the integers with,besides other monotone operators,addition, multiplication by positive constants, maximum, and minimum.The algorithm is based on max-strategy iteration.Its worst-case running-time (w.r.t. a uniform cost measure)is independent of the sizes of occurring numbers.We apply thisalgorithm to compute the abstract semantics ofprograms over integer intervals as well as over integer zones.

scholarly journals Optimal Purely Functional Priority Queues

1996 ◽  
Vol 3 (37) ◽  
Author(s):  
Gerth Stølting Brodal ◽  
Chris Okasaki
Keyword(s):  
Data Structure ◽  
Higher Order ◽  
Priority Queues ◽  
Worst Case ◽  
Minimum Element ◽  
Asymptotically Optimal ◽  
Running Time ◽  
Recursive Structures ◽  
Functional Setting

Brodal recently introduced the first implementation of imperative priority queues to support findMin, insert, and meld in O(1) worst-case time, and deleteMin in O(log n) worst-case time. These bounds are asymptotically optimal among all comparison-based priority queues. In this paper, we adapt<br />Brodal's data structure to a purely functional setting. In doing so, we both simplify the data structure and clarify its relationship to the binomial queues of Vuillemin, which support all four operations in O(log n) time. Specifically, we derive our implementation from binomial queues in three steps: first, we reduce the running time of insert to O(1) by eliminating the possibility of cascading links; second, we reduce the running time of findMin to O(1) by adding a global root to hold the minimum element; and finally, we reduce the running time of meld to O(1) by allowing priority queues to contain other<br />priority queues. Each of these steps is expressed using ML-style functors. The last transformation, known as data-structural bootstrapping, is an interesting<br />application of higher-order functors and recursive structures.

scholarly journals Abstract interpretation of temporal concurrent constraint programs

2014 ◽  
Vol 15 (3) ◽  
pp. 312-357 ◽  
Author(s):  
MORENO FALASCHI ◽  
CARLOS OLARTE ◽  
CATUSCIA PALAMIDESSI
Keyword(s):  
Abstract Interpretation ◽  
Data Flow ◽  
Reactive Systems ◽  
Security Protocols ◽  
Denotational Semantics ◽  
Security Protocol ◽  
Mobile Systems ◽  
Abstract Domains ◽  
Concurrent Constraint Programming ◽  
Abstract Semantics

AbstractTimed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e., systems that continuously interact with the environment. The universaltccformalism (utcc) is an extension oftccwith the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics fortcc, and extend it to a “collecting” semantics forutccbased on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses oftccandutccprograms by abstract interpretation techniques. The concrete and abstract semantics that we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis fortccprograms. We show the applicability of this analysis in the context of reactive systems. Furthermore, we also make use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show thattccprograms are suspension-free. This can be useful for several purposes, such as for optimizing compilation or for debugging.

scholarly journals Exploiting reachability and cardinality in higher-order flow analysis

2008 ◽  
Vol 18 (5-6) ◽  
pp. 821-864 ◽  
Author(s):  
MATTHEW MIGHT ◽  
OLIN SHIVERS
Keyword(s):  
Abstract Interpretation ◽  
Garbage Collection ◽  
Flow Analysis ◽  
Higher Order ◽  
Order Flow ◽  
Environment Analysis ◽  
Running Time

AbstractWe present two complementary improvements for abstract-interpretation-based flow analysis of higher-order languages: (1) abstract garbage collection and (2) abstract counting. Abstract garbage collection is an analog to its concrete counterpart: the analysis determines when an abstract resource has become unreachable, and then, re-allocates it as fresh. This prevents flow sets from joining during abstract interpretation, which has two immediate effects: (1) the precision of the interpretation increases and (2) its running time often falls. In abstract counting, the analysis tracks how many times an abstract resource has been allocated. A count of one implies that the abstract resource momentarily represents only one concrete resource. This knowledge, in turn, drives environment analysis, expanding the kind (rather than just the degree) of optimization available to the compiler.

scholarly journals Efficiency Through Procrastination: Approximately Optimal Algorithm Configuration with Runtime Guarantees

2017 ◽  
Author(s):  
Robert Kleinberg ◽  
Kevin Leyton-Brown ◽  
Brendan Lucier
Keyword(s):  
High Probability ◽  
Optimal Algorithm ◽  
Optimal Performance ◽  
Worst Case ◽  
Running Time ◽  
Performance Guarantees ◽  
Algorithm Configuration ◽  
Time Requirements

Algorithm configuration methods have achieved much practical success, but to date have not been backed by meaningful performance guarantees. We address this gap with a new algorithm configuration framework, Structured Procrastination. With high probability and nearly as quickly as possible in the worst case, our framework finds an algorithm configuration that provably achieves near optimal performance. Moreover, its running time requirements asymptotically dominate those of existing methods.

scholarly journals Fitness Conditions for fixed Point Iteration

1992 ◽  
Vol 21 (384) ◽  
Author(s):  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Fixed Point ◽  
Abstract Interpretation ◽  
Flow Analysis ◽  
Worst Case ◽  
Fixed Point Iteration ◽  
Average Case ◽  
Data Flow Analysis ◽  
Tail Recursion ◽  
Carry Over ◽  
Primitive Recursive

This paper provides a link between the formulation of static program analyses using the framework of abstract interpretation (popular for functional languages) and using the more classical framework of data flow analysis (popular for imperative languages). In particular we show how the classical notions of fastness, rapidity and k-boundedness carry over to the abstract interpretation framework and how this may be used to bound the number of times a functional should be unfolded in order to yield the fixed point. This is supplemented with a number of results on how to calculate the bounds for iterative forms (as for tail recursion), for linear forms (as for one nested recursive call), and for primitive recursive forms. In some cases this improves the ''worst case'' results of H.R. Nielson and F. Nielson: Bounded Fixed Point Iteration, but more importantly it gives much better ''average case'' results.

scholarly journals The Uses of SAT Solvers in Vampire

10.29007/4w68 ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Data Structures ◽  
Theorem Prover ◽  
Worst Case ◽  
Running Time ◽  
First Order ◽  
Sat Solvers ◽  
Memory Overhead ◽  
Complex Term

Reasoning in a saturation-based first-order theorem prover is generally expensive involving complex term-indexing data structures and inferences such as subsumption resolution whose (worst case) running time is exponential in the length of the clause. In contrast, SAT solvers are very cheap, being able to solve large problems quickly and with relatively little memory overhead.Consequently, utilising this cheap power within Vampire to carry out certain tasks has proven highly successful. We give an overview of the different ways that SAT solvers are utilisedwithin Vampire and discuss further ways in which this usage could be extended

Chapter 16. Worst-Case Upper Bounds

2021 ◽  
Author(s):  
Evgeny Dantsin ◽  
Edward A. Hirsch
Keyword(s):  
Structural Complexity ◽  
Upper Bounds ◽  
Worst Case ◽  
Exponential Time ◽  
Running Time ◽  
Dichotomy Theorem ◽  
Exponential Time Hypothesis ◽  
Satisfiability Algorithms

The chapter is a survey of ideas and techniques behind satisfiability algorithms with the currently best asymptotic upper bounds on the worst-case running time. The survey also includes related structural-complexity topics such as Schaefer’s dichotomy theorem, reductions between various restricted cases of SAT, the exponential time hypothesis, etc.

ISOMORPHIC TRIANGULATIONS WITH SMALL NUMBER OF STEINER POINTS

1999 ◽  
Vol 09 (02) ◽  
pp. 171-180 ◽  
Author(s):  
EVANGELOS KRANAKIS ◽  
JORGE URRUTIA
Keyword(s):  
Worst Case ◽  
Running Time ◽  
Steiner Points ◽  
Simple Polygons

Assume that an isomorphism between two n-vertex simple polygons, P,Q (with k,l reflex vertices, respectively) is given. We present two algorithms for constructing isomorphic (i.e. adjacency preserving) triangulations of P and Q, respectively. The first algorithm computes isomorphic triangulations of P and Q by introducing at most O((k+l)2) Steiner points and has running time O(n+(k+l)2). The second algorithm computes isomorphic traingulations of P and Q by introducing at most O(kl) Steiner points and has running time O(n+kl log n). The number of Steiner points introduced by the second algorithm is also worst-case optimal. Unlike the O(n2) algorithm of Aronov, Seidel and Souvaine1 our algorithms are sensitive to the number of reflex vertices of the polygons. In particular, our algorithms have linear running time when [Formula: see text] for the first algorithm, and kl≤n/ log  n for the second algorithm.

Sign in / Sign up

Export Citation Format

Share Document