Abstract Flow-sensitive and flow-insensitive analyses of programs occupy opposite ends of a spectrum. Between these extremes lie mixed flow sensitive approaches, where some aspects of program behavior are analyzed flow-insensitively and others flow-sensitively. Mixed flow-sensitivity arises, for example, in the analysis of multi-threaded code or code withnon-local control flow. Another instance is global store widening for efficient analysis of functional languages and some forms of pointer analysis. While mixed flow-sensitive analyses are common in the literature, the formulation of the particular analysis problem and the means to solve it are often tightly coupled. Side-effecting constraint systems provide a generic mechanism for describing mixed flow-sensitive analyses, thus decoupling the analysis definition from solver algorithm details. The abstract interpreter Goblint realizes this decoupling, and allows defining mixed flow-sensitive analyses independently of generic solvers. We indicate how the precision of specified analyses can be improved using digests (on the side of the formulation of the analysis problem) and suitable update rules (on the side of the solver). We explain how developers can use Goblint to implement their own mixed flow-sensitive analyses.

Abstract The top-down solver TD is a generic fixpoint algorithm that can be used to compute partial post-solutions of equation systems for abstract interpretation. We consider two extensions of the TD to deal with infinite strictly ascending chains. For the TD extended with warrowing , we formally prove that it always returns partial post-solutions, while for the TD extended with widening and narrowing in phases, we prove termination provided that the set of unknowns is finite. By proving the equivalence of the two extensions, we deduce the total correctness of both solvers. For the equivalence to hold, we in particular assume the equation system to have right-hand sides that are both monotonic and have monotonic dependencies . We demonstrate with counterexamples that the violation of any of the assumptions may compromise the equivalence. All proofs have been formalized using the interactive theorem prover Isabelle.

Abstract First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of occurring negated literals decreases in every iteration, or the number of required instances of input predicates or the number of first-order variables remains bounded. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed. We apply these results to identify classes of multi-agent systems, when formalized as first-order transition systems, where noninterference in presence of declassification is decidable for coalitions of attackers of bounded size.

Static analysis of real-world programs combines flow- and context-sensitive analyses of local program states with computation of flow- and context-insensitive invariants at globals , that, e.g., abstract data shared by multiple threads. The values of locals and globals may mutually depend on each other, with the analysis of local program states both making contributions to globals and querying their values. Usually, all contributions to globals are accumulated during fixpoint iteration, with widening applied to enforce termination. Such flow-insensitive information often becomes unnecessarily imprecise and can include superfluous contributions — trash — which, in turn, may be toxic to the precision of the overall analysis. To recover precision of globals, we propose techniques complementing each other: Narrowing on globals differentiates contributions by origin; reluctant widening limits the amount of widening applied at globals; and finally, abstract garbage collection undoes contributions to globals and propagates their withdrawal. The experimental evaluation shows that these techniques increase the precision of mixed flow-sensitive analyses at a reasonable cost.

Abstract Context-sensitive analysis of programs containing recursive procedures may be expensive. This may particularly be the case when expressive domains are used, rendering the set of possible contexts large or even infinite. Here we present a framework for context-sensitivity and, as a base step, show how to formalize full contexts, partial contexts, and call strings in it. In this framework, we propose three generic lifters that allow bounding the number of encountered contexts for existing analyses on the fly, i.e., without requiring a preanalysis: Context Widening, Loopfree Callsting, and Context Gas. The proposed analysis lifters maintain the soundness of the underlying base analyses. For these approaches, we prove that only finitely many function contexts are encountered during fixpoint iteration—a key requirement for termination—when the fixpoint iteration is known to update the value of each unknown only a finite number of times. Context Gas and friends are implemented within the abstract interpreter Goblint and compared to existing approaches to context-sensitivity on the SV-COMP benchmark suite. On a subset of recursive benchmarks, all proposed lifters manage to reduce the number of stack overflows and timeouts compared to a full context approach, with one configuration of the Context Gas approach improving the number of correct verdicts by $31\%$ 31 % and showing promising results on the considered SV-COMP categories.

Abstract The top-down solver (TD) is a local fixpoint algorithm for arbitrary equation systems. It considers the right-hand sides as black boxes and detects dependencies between unknowns on the fly—features that significantly increase both its usability and practical efficiency. At the same time, the recursive evaluation strategy of the TD, combined with the non-local destabilization mechanism, obfuscates the correctness of the computed solution. To strengthen the confidence in tools relying on the TD as their fixpoint engine, we provide a first machine-checked proof of the partial correctness of the TD. Our proof builds on the observation that the TD can be obtained from a considerably simpler recursive fixpoint algorithm, the plain TD, by applying an optimization that neither affects the termination behavior nor the computed result. Accordingly, we break down the proof into a partial correctness proof of the plain TD, which is only then extended to include the optimization. The backbone of our proof is a mutual induction following the solver’s computation trace. We establish sufficient invariants about the solver state to conclude the correctness of its optimization, i.e., the plain TD terminates if and only if the TD terminates, and they return the identical result. The proof is written using Isabelle/HOL and is available in the archive of formal proofs.

Abstract Goblintis an abstract interpretation framework for C programs with a specialty in concurrency. Using a novel approach, we turn it into a validator of YAML correctness witnesses for all SV-COMP categories. We describe its results at SV-COMP 2024 which includes the first large-scale evaluation of our validator.

Abstract Goblintis an abstract interpreter of C programs, focusing on the analysis of multi-threaded code. It is equipped with a variety of abstract domains, as well as analyses which allow it to reason about an array of program properties in a highly configurable manner.Goblinthas been extended with support for the detection of memory safety bugs and non-termination.

We prove that functionality of compositions of top-down tree transducers is decidable by reducing the problem to the functionality of one top-down tree transducer with look-ahead.

We show that every prenex universal syntactic first-order safety property can be compiled into a universal invariant of a first-order transition system using quantifier-free substitutions only. We apply this insight to prove that every such safety property is decidable for first-order transition systems with stratified guarded updates only.

It is well known that for a given bottom-up tree automaton it can be decided whether or not an equivalent deterministic top-down tree automaton exists. Recently it was claimed that such a decision can be carried out in polynomial time (Leupold and Maneth, FCT'2021); but their procedure and corresponding property is wrong. Here we address this mistake and present a correct property which allows to determine in polynomial time whether or not a given tree language can be recognized by a deterministic top-down tree automaton. Furthermore, our new property is stated for arbitrary deterministic bottom-up tree automata, and not only for minimal such automata (as before).

Abstract To put sound program analysis at the fingertips of the software developer, we propose a framework for interactive abstract interpretation of multithreaded C code. Abstract interpretation provides sound analysis results, but can be quite costly in general. To achieve quick response times, we incrementalize the analysis infrastructure, including postprocessing, without necessitating any modifications to the analysis specifications themselves. We rely on the local generic fixpoint engine TD – which we enhance with reluctant destabilization to minimize reanalysis effort. Dedicated further improvements support precise incremental analysis of program properties that include concurrency deficiencies such as data-races. The framework has been implemented in the static analyzer Goblint, and combined with the MagpieBridge framework to relay findings to IDEs. We evaluate our implementation w.r.t. the yard sticks of response time and consistency. We also provide examples of program development highlighting the usability of our approach.

Abstract The C programming language offers as a mechanism for nonlocal control flow. This mechanism has complicated semantics. As most developers do not encounter it day-to-day, they may be unfamiliar with all its intricacies – leading to subtle programming errors. At the same time, most static analyzers lack proper support, implying that otherwise sound tools miss whole classes of program deficiencies. We propose a concrete semantics of a subset of C with , where interprocedural s are performed directly, as well as an equivalent formulation where such jumps are implemented via stack-unwinding at the call-sites. Reflecting this semantic equivalence, we propose an approach for lifting existing interprocedural analyses to support and to flag their misuse. To deal with the nonlocal semantics, our approach leverages side-effecting transfer functions, which, when executed, may additionally trigger contributions for program points that are not static control-flow successors. We showcase our analysis on a real-world example and propose a set of litmus tests for other analyzers.

Abstract The weakly relational domain of Octagons offers a decent compromise between precision and efficiency for numerical properties. Here, we are concerned with the construction of non-numerical relational domains. We provide a general construction of weakly relational domains, which we exemplify with an extension of constant propagation by disjunctions. Since for the resulting domain of 2-disjunctive formulas satisfiability is NP-complete, we provide a general construction for a further, more abstract, weakly relational domain where the abstract operations of restriction and least upper bound can be efficiently implemented. In the second step, we consider a relational domain that tracks conjunctions of inequalities between variables, and between variables and constants for arbitrary partial orders of values. Examples are sub(multi)sets, as well as prefix, substring or scattered substring orderings on strings. When the partial order is a lattice, we provide precise polynomial algorithms for satisfiability, restriction, and the best abstraction of disjunction. Complementary to the constructions for lattices, we find that, in general, satisfiability of conjunctions is NP-complete. We therefore again provide polynomial abstract versions of restriction, conjunction, and join. By using our generic constructions, these domains are extended to weakly relational domains that additionally track disjunctions. For all our domains, we indicate how abstract transformers for assignments and guards can be constructed.

Abstract We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables – given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.

Abstract The static analyzer Goblint is dedicated to the analysis of multi-threaded C programs by abstract interpretation. It provides multiple techniques for increasing analysis precision, e.g., configurable context-sensitivity and a wide range of numerical analyses. As a rule of thumb, more precise analyses decrease scalability, while not always necessary for solving the task at hand. Therefore, Goblint has been enhanced with autotuning which, based on syntactical criteria, adapts analysis configuration to the given program such that relevant precision is obtained with acceptable effort.

We consider a notion of origin for deterministic macro tree transducers with look-ahead which records for each output node, the corresponding input node for which a rule-application generated that output node. With respect to this natural notion, we show that “origin equivalence” is decidable — whenever the transducers are weakly self-nesting. The latter means that whenever two nested calls on the same input node occur, then there must be at least one other node (a terminal output node or a call on another input node) in between these nested calls. Besides origin equivalence we are also able to decide “origin injectivity” for such transducers.

Abstract Goblintis a static analysis framework for C programs specializing in data race analysis. It relies on thread-modular abstract interpretation where thread interferences are accounted for by means of flow-insensitive global invariants.

Abstract The local solver TD is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD gains efficiency by detecting dependencies between unknowns on the fly. This algorithm has been recently extended to deal with widening and narrowing as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many unknowns are encountered, and all right-hand sides are monotonic . While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all encountered unknowns instead of a minimal set sufficient for performing the iteration. By consuming unnecessarily much space, interprocedural analyses may not succeed on seemingly small programs. In the present paper, we therefore extend the top-down solver TD in three ways. First, we indicate how the restriction to monotonic right-hand sides can be lifted without compromising termination. We then show how the solver can be tuned to store abstract values only when their preservation is inevitable. Finally, we also show how the solver can be extended to side-effecting equation systems. Right-hand sides of these may not only provide values for the corresponding left-hand side unknowns but at the same time produce contributions to other unknowns. This practical extension has successfully been used for a seamless combination of context-sensitive analyses (e.g., of local states) with flow-insensitive analyses (e.g., of globals).

We consider two natural subclasses of deterministic top-down tree-to-tree transducers, namely, linear and uniform-copying transducers. For both classes we show that it is decidable whether the translation of a transducer with look-ahead can be realized by a transducer without look-ahead. The transducers constructed in this way, may still make use of inspection, i.e., have an additional tree automaton restricting the domain. We provide a second procedure which decides whether inspection can be removed and if so, constructs an equivalent transducer without inspection. The construction relies on a fixpoint algorithm that determines inspection requirements and on dedicated earliest normal forms for linear as well as uniform-copying transducers which can be constructed in polynomial time. As a consequence, equivalence of these transducers can be decided in polynomial time. Applying these results to deterministic bottom-up transducers, we obtain that it is decidable whether or not their translations can be realized by deterministic uniform-copying top-down transducers without look-ahead (but with inspection) - or without both look-ahead and inspection.

Abstract We present an automated procedure for synthesizing sound inductive invariants for floating-point numerical loops. Our procedure generates invariants of the form of a convex polynomial inequality that tightly bounds the values of loop variables. Such invariants are a prerequisite for reasoning about the safety and roundoff errors of floating-point programs. Unlike previous approaches that rely on policy iteration, linear algebra or semi-definite programming, we propose a heuristic procedure based on simulation and counterexample-guided refinement. We observe that this combination is remarkably effective and general and can handle both linear and nonlinear loop bodies, nondeterministic values as well as conditional statements. Our evaluation shows that our approach can efficiently synthesize loop invariants for existing benchmarks from literature, but that it is also able to find invariants for nonlinear loops that today’s tools cannot handle.

Abstract First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of first-order variables, or the number of required instances of input predicates remains bounded, or the number of occurring negated literals decreases in every iteration. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed.

Abstract In 1982, Courcelle and Franchi-Zannettacci showed that the equivalence problem of separated non-nested attribute systems can be reduced to the equivalence problem of total deterministic separated basic macro tree transducers. They also gave a procedure for deciding equivalence of transducer in the latter class. Here, we reconsider this equivalence problem. We present a new alternative decision procedure and prove that it runs in polynomial time. We also consider extensions of this result to partial transducers and to the case where parameters of transducers accumulate strings instead of trees.

Our goal is to certify absence of information leaks in multi-agent workflows, such as conference management systems like EasyChair. These workflows can be executed by any number of agents some of which may form coalitions against the system. Therefore, checking noninterference is a challenging problem. Our paper offers two main contributions: First, a technique is provided to translate noninterference (in presence of various agent capabilities and declassification conditions) into universally quantified invariants of an instrumented new workflow program. Second, general techniques are developed for checking and inferring universally quantified inductive invariants for workflow programs. In particular, a large class of workflows is identified where inductiveness of invariants is decidable, as well as a smaller, still useful class of workflows where the weakest inductive universal invariant implying the desired invariant, is effectively computable. The new algorithms are implemented and applied to certify noninterference for workflows arising from conference management systems.

The local solver TD is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD gains efficiency by detecting variable dependencies on the fly. This algorithm has been recently extended to deal with widening and narrowing as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many variables are encountered, and all right-hand sides are monotonic. While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all encountered variables in one data-structure --- thus prohibiting interprocedural analyses to scale to larger programs.

We present two structural results concerning longest common prefixes of non-empty languages. First, we show that the longest common prefix of the language generated by a context-free grammar of size $N$ equals the longest common prefix of the same grammar where the heights of the derivation trees are bounded by $4N$. Second, we show that each nonempty language $L$ has a representative subset of at most three elements which behaves like $L$ w.r.t. the longest common prefix as well as w.r.t. longest common prefixes of $L$ after unions or concatenations with arbitrary other languages. From that, we conclude that the longest common prefix, and thus the longest common suffix, of a context-free language can be computed in polynomial time.

We prove that equivalence of deterministic top-down tree-to-string transducers is decidable, thus solving a long-standing open problem in formal language theory. We also present efficient algorithms for subclasses: for linear transducers or total transducers with unary output alphabet (over a given top-down regular domain language), as well as for transducers with the single-use restriction. These results are obtained using techniques from multi-linear algebra. For our main result, we introduce polynomial transducers and prove that for these, validity of a polynomial invariant can be certified by means of an inductive invariant of polynomial ideals. This allows us to construct two semi-algorithms, one searching for a certificate of the invariant and one searching for a witness of its violation. Via a translation into polynomial transducers, we thus obtain that equivalence of general y dt transducers is decidable. In fact, our translation also shows that equivalence is decidable when the output is not in a free monoid but in a free group.

It is well known that satisfiability is decidable for Horn clauses of the class . Since arbitrary Horn clauses can naturally be approximated by -clauses, can be used for realizing any program analysis which can be specified by means of Horn clauses. Recently, we have shown that decidability for Horn clauses from is retained if the clauses are either extended with tests for disequality between subterms identified by paths or for disequality between homomorphic images of terms. These two results refer to orthogonal extensions of -clauses. Here, we provide a generalization of both results. For that, we introduce hom-path disequalities and show that for each finite set of -clauses extended with such tests an equivalent tree automaton with hom-path disequalities can be constructed. Since emptiness for that class of automata has been shown decidable by Godoy et al. in 2010, we conclude that satisfiability is decidable for -clauses with hom-path disequalities.

We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an unbounded number of participating agents. The information flow policies are specified in a temporal logic for hyperproperties. We show that the verification problem can be reduced to the satisfiability of a formula of first-order linear-time temporal logic, and provide decidability results for relevant classes of workflows and specifications. We report on experimental results obtained with an implementation of our approach on a series of benchmarks.

Device drivers rely on fine-grained locking to ensure safe access to shared data structures. For human testers, concurrency makes such code notoriously hard to debug; for automated reasoning, dynamically allocated memory and low-level pointer manipulation poses significant challenges. We present a flexible approach to data race analysis, implemented in the open source Goblint static analysis framework, that combines different pointer and value analyses in order to handle a wide range of locking idioms, including locks allocated dynamically as well as locks stored in arrays. To the best of our knowledge, this is the most ambitious effort, having lasted well over ten years, to create a fully automated static race detection tool that can deal with most of the intricate locking schemes found in Linux device drivers. Our evaluation shows that these analyses are sufficiently precise, but practical use of these techniques requires inferring environmental and domain-specific assumptions.

We introduce a novel way of proving information flow properties of a program based on its self-composition. Similarly to the universal information flow type system of Hunt and Sands, our analysis explicitly computes the dependencies of variables in the final state on variables in the initial state. Accordingly, the analysis result is independent of specific information flow lattices, and allows to derive information flow w.r.t. any of these. While our analysis runs in polynomial time, we prove that it never loses precision against the type system of Hunt and Sands, and may gain extra precision by taking similarities between different branches of conditionals into account. Also, we indicate how it can be smoothly generalized to an interprocedural analysis.

We show that equivalence of deterministic top-down tree-to-string transducers is decidable, thus solving a long standing open problem in formal language theory. We also present efficient algorithms for subclasses: polynomial time for total transducers with unary output alphabet (over a given top-down regular domain language), and co-randomized polynomial time for linear transducers, these results are obtained using techniques from multi-linear algebra. For our main result, we prove that equivalence can be certified by means of inductive invariants using polynomial ideals. This allows us to construct two semi-algorithms, one searching for a proof of equivalence, one for a witness of non-equivalence.

Information flow properties of programs can be formalized as hyperproperties specifying the relation of multiple executions. In this paper, we therefore introduce a framework for proving 2-hypersafety properties by means of abstract interpretation. The main idea is to apply abstract interpretation on the self-compositions of the control flow graphs of programs. As a result, our method is inherently capable of analyzing relational properties of even dissimilar programs.

Non-trivial analysis problems require complete lattices with infinite ascending and descending chains. In order to compute reasonably precise post-fixpoints of the resulting systems of equations, Cousot and Cousot have suggested accelerated fixpoint iteration by means of widening and narrowing.

We consider programs for embedded real-time systems which use priority-driven preemptive scheduling with task priorities adjusted dynamically according to the immediate ceiling priority protocol. For these programs, we provide static analyses for detecting data races between tasks running at different priorities as well as methods to guarantee transactional execution of procedures. Beyond that, we demonstrate how general techniques for value analyses can be adapted to this setting by developing a precise analysis of affine equalities.

In this article we provide an interprocedural analysis of linear two-variable equalities. The novel algorithm has a worst-case complexity of 𝒪( n ⋅ k 4 ), where k is the number of variables and n is the program size. Thus, it saves a factor of k 4 in comparison to a related algorithm based on full linear algebra. We also indicate how the practical runtime can be further reduced significantly. The analysis can be applied, for example, for register coalescing, for identifying local variables and thus for interprocedurally observing stack pointer modifications as well as for an analysis of array index expressions, when analyzing low-level code.

We present practical algorithms for computing exact least solutions of equation systems over the reals with addition, multiplication by positive constants, minimum and maximum. The algorithms are based on strategy iteration. Our algorithms can, for instance, be used for the analysis of recursive stochastic games. In the present article we apply our techniques for computing abstract least fixpoint semantics of affine programs over the relational template polyhedra domain. In particular, we thus obtain practical algorithms for computing abstract least fixpoint semantics over the abstract domains of intervals, zones, and octagons.

Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class C of first-order clauses. They showed its satisfiability problem to be in 3-DEXPTIME. We improve this result by showing that satisfiability for this class is NEXPTIME-complete, using new resolution techniques. We show satisfiability to be DEXPTIME-complete if clauses are Horn, which is what is required for modeling cryptographic protocols. While translation to Horn clauses only gives a DEXPTIME upper bound for the secrecy problem for these protocols, we further show that this secrecy problem is actually DEXPTIME-complete.

We consider integer arithmetic modulo a power of 2 as provided by mainstream programming languages like Java or standard implementations of C. The difficulty here is that, for w > 1, the ring Z m of integers modulo m = 2 w has zero divisors and thus cannot be embedded into a field. Not withstanding that, we present intra- and interprocedural algorithms for inferring for every program point u affine relations between program variables valid at u . If conditional branching is replaced with nondeterministic branching, our algorithms are not only sound but also complete in that they detect all valid affine relations in a natural class of programs. Moreover, they run in time linear in the program size and polynomial in the number of program variables and can be implemented by using the same modular integer arithmetic as the target language to be analyzed. We also indicate how our analysis can be extended to deal with equality guards, even in an interprocedural setting.

MSO logic on unranked trees has been identified as a convenient theoretical framework for reasoning about expressiveness and implementations of practical XML query languages. As a corresponding theoretical foundation of XML transformation languages, the "transformation language" TL is proposed. This language is based on the "document transformation language" DTL of Maneth and Neven which incorporates full MSO pattern matching, arbitrary navigation in the input tree using also MSO patterns, and named procedures. The new language generalizes DTL by additionally allowing procedures to accumulate intermediate results in parameters. It is proved that TL -- and thus in particular DTL - despite their expressiveness still allow for effective inverse type inference. This result is obtained by means of a translation of TL programs into compositions of top-down finite state tree transductions with parameters, also called (stay) macro tree transducers.

We apply linear algebra techniques to precise interprocedural dataflow analysis. Specifically, we describe analyses that determine for each program point identities that are valid among the program variables whenever control reaches that program point. Our analyses fully interpret assignment statements with affine expressions on the right hand side while considering other assignments as non-deterministic and ignoring conditions at branches. Under this abstraction, the analysis computes the set of all affine relations and, more generally, all polynomial relations of bounded degree precisely. The running time of our algorithms is linear in the program size and polynomial in the number of occurring variables. We also show how to deal with affine preconditions and local variables and indicate how to handle parameters and return values of procedures.

A query against a database behind a site like Napster may search, e.g., for all users who have downloaded more jazz titles than pop music titles. In order to express such queries, we extend classical monadic second-order logic by Presburger predicates which pose numerical restrictions on the children (content) of an element node and provide a precise automata-theoretic characterization. While the existential fragment of the resulting logic is decidable, it turns out that satisfiability of the full logic is undecidable. Decidable satisfiability and a querying algorithm even with linear data complexity can be obtained if numerical constraints are only applied to those contents of elements where ordering is irrelevant. Finally, it is sketched how these techniques can be extended also to answer questions like, e.g., whether the total price of the jazz music downloaded so far exceeds a user's budget.

Optimal program slicing determines for a statement S in a program π whether or not S affects a specified set of statements, given that all conditionals in π are interpreted as non-deterministic choices.

Wadler's deforestation algorithm removes intermediate data structures from functional programs. To be appropriate for inclusion in a compiler, deforestation must terminate on all programs. Several techniques exist to ensure termination of deforestation on all first-order programs, but a technique for higher-order programs was only recently introduced by Hamilton and later Marlow. We present a new technique for ensuring termination of deforestation on all higher-order programs that allows useful transformation steps prohibited in Hamilton's and Marlow's techniques. The technique uses a constraint-based higher-order control-flow analysis. 1 Introduction Lazy, higher-order, functional programming languages lend themselves to a certain style of programming which uses intermediate data structures [28]. However, this style also leads to inefficient programs. Example 1 Consider the following program. letrec a = x; y: case x of [] ! y (h : t) ! h : a t y in u; v; w: a (a u v) w The mai...

Durational transition systems are finite transition systems where every transition is additionally equipped with a duration. We consider the problem of interpreting /spl mu/-formulas over durational transition systems. In case the formula contains only operations minimum, maximum, addition, and sequencing, we show that the interpretation ist not only computable but (up to a linear factor) as efficiently computable as the interpretation of /spl mu/-formulas over ordinary finite transition systems.

It is shown that for every constant m it can be decided in polynomial time whether or not two m-ambiguous finite tree automata are equivalent. In general, inequivalence for finite tree automata is DEXPTIME-complete with respect to logspace reductions, and PSPACE-complete with respect to logspace reductions, if the automata in question are supposed to accept only finite languages. For finite tree automata with weights in a field R, a polynomial time algorithm is presented for deciding ambiguity-equivalence, provided R-operations and R-tests for 0 can be performed in constant time. This result is used to construct an algorithm deciding ambiguity-inequivalence of finite tree automata in randomized polynomial time. Finally, for every constant m it is shown that it can be decided in polynomial time whether or not a given finite tree automaton is m-ambiguous.