Showing 1–23 of 23 results for author: Seidl, H

Non-Numerical Weakly Relational Domains

Authors: Helmut Seidl, Julian Erhard, Sarah Tilscher, Michael Schwarz

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 f… ▽ More 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. △ Less

Submitted 10 January, 2024; originally announced January 2024.

Comments: 15 pages

ACM Class: F.3.1

Correctness Witness Validation by Abstract Interpretation

Authors: Simmo Saan, Michael Schwarz, Julian Erhard, Helmut Seidl, Sarah Tilscher, Vesal Vojdani

Abstract: Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We dem… ▽ More Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own. △ Less

Submitted 25 October, 2023; originally announced October 2023.

Comments: 29 pages, 4 figures, 2 tables, extended version of the paper which is to appear at VMCAI 2024

Checking in Polynomial Time whether or not a Regular Tree Language is Deterministic Top-Down

Authors: Sebastian Maneth, Helmut Seidl

Abstract: It is well known that for a given bottom-up tree automaton it can be decided whether or not there exists deterministic top-down tree automaton that recognized the same tree language. 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 correct this mistake and present a co… ▽ More It is well known that for a given bottom-up tree automaton it can be decided whether or not there exists deterministic top-down tree automaton that recognized the same tree language. 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 correct 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 for minimal such automata (as before). △ Less

Submitted 1 June, 2023; originally announced June 2023.

Clustered Relational Thread-Modular Abstract Interpretation with Local Traces

Authors: Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard, Vesal Vojdani

Abstract: We construct novel thread-modular analyses that track relational information for potentially overlap** 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 dynami… ▽ More We construct novel thread-modular analyses that track relational information for potentially overlap** 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. △ Less

Submitted 16 January, 2023; originally announced January 2023.

Comments: Extended version of the paper with the same name which is to appear at ESOP '23

Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap

Authors: Julian Erhard, Simmo Saan, Sarah Tilscher, Michael Schwarz, Karoliine Holter, Vesal Vojdani, Helmut Seidl

Abstract: To put static program analysis at the fingertips of the software developer, we propose a framework for interactive abstract interpretation. While providing sound analysis results, abstract interpretation in general can be quite costly. To achieve quick response times, we incrementalize the analysis infrastructure, including postprocessing, without necessitating any modifications to the analysis sp… ▽ More To put static program analysis at the fingertips of the software developer, we propose a framework for interactive abstract interpretation. While providing sound analysis results, abstract interpretation in general can be quite costly. 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 dynamically tracks dependencies, while exploring the unknowns contributing to answering an initial query. Lazy invalidation is employed for analysis results affected by program change. Dedicated improvements support the incremental analysis of concurrency deficiencies such as data-races. The framework has been implemented for multithreaded C within the static analyzer Goblint, using MagpieBridge to relay findings to IDEs. We evaluate our implementation w.r.t. the yard sticks of response time and consistency: formerly proven invariants should be retained - when they are not affected by the change. The results indicate that with our approach, a reanalysis after small changes only takes a fraction of from-scratch analysis time, while most of the precision is retained. We also provide examples of program development highlighting the usability of the overall approach. △ Less

Submitted 25 November, 2022; v1 submitted 21 September, 2022; originally announced September 2022.

Comments: 16 pages, 9 figures

ACM Class: D.2.4

How to decide Functionality of Compositions of Top-Down Tree Transducers

Authors: Sebastian Maneth, Helmut Seidl, Martin Vu

Abstract: 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 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. △ Less

Submitted 2 September, 2022; originally announced September 2022.

Improving Thread-Modular Abstract Interpretation

Authors: Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani

Abstract: We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Miné's approach can be obtained as instances of thi… ▽ More We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Miné's approach can be obtained as instances of this general scheme. We show that these two analyses are incomparable w.r.t. precision and provide a refinement which improves on both precision-wise. We also report on a preliminary experimental comparison of the given analyses on a meaningful suite of benchmarks. △ Less

Submitted 17 August, 2021; originally announced August 2021.

Comments: This is the extended version of a paper with the same title accepted at SAS'2021

Definability Results for Top-Down Tree Transducers

Authors: Sebastian Maneth, Helmut Seidl, Martin Vu

Abstract: We prove that for a given deterministic top-down transducer with look-ahead it is decidable whether or not its translation is definable (1)~by a linear top-down tree transducer or (2)~by a tree homomorphism. We present algorithms that construct equivalent such transducers if they exist. We prove that for a given deterministic top-down transducer with look-ahead it is decidable whether or not its translation is definable (1)~by a linear top-down tree transducer or (2)~by a tree homomorphism. We present algorithms that construct equivalent such transducers if they exist. △ Less

Submitted 31 May, 2021; originally announced May 2021.

Equivalence of Linear Tree Transducers with Output in the Free Group

Authors: Raphaela Löbel, Michael Luttenberger, Helmut Seidl

Abstract: We show that equivalence of deterministic linear tree transducers can be decided in polynomial time when their outputs are interpreted over the free group. Due to the cancellation properties offered by the free group, the required constructions are not only more general, but also simpler than the corresponding constructions for proving equivalence of deterministic linear tree-to-word transducers. We show that equivalence of deterministic linear tree transducers can be decided in polynomial time when their outputs are interpreted over the free group. Due to the cancellation properties offered by the free group, the required constructions are not only more general, but also simpler than the corresponding constructions for proving equivalence of deterministic linear tree-to-word transducers. △ Less

Submitted 13 March, 2020; v1 submitted 10 January, 2020; originally announced January 2020.

Comments: Minor changes based on some reviews. A short version of this paper will be published in the proceedings of DLT 2020

On the Balancedness of Tree-to-word Transducers

Authors: Raphaela Löbel, Michael Luttenberger, Helmut Seidl

Abstract: A language over an alphabet $B = A \cup \overline{A}$ of opening ($A$) and closing ($\overline{A}$) brackets, is balanced if it is a subset of the Dyck language $D_B$ over $B$, and it is well-formed if all words are prefixes of words in $D_B$. We show that well-formedness of a context-free language is decidable in polynomial time, and that the longest common reduced suffix can be computed in polyn… ▽ More A language over an alphabet $B = A \cup \overline{A}$ of opening ($A$) and closing ($\overline{A}$) brackets, is balanced if it is a subset of the Dyck language $D_B$ over $B$, and it is well-formed if all words are prefixes of words in $D_B$. We show that well-formedness of a context-free language is decidable in polynomial time, and that the longest common reduced suffix can be computed in polynomial time. With this at a hand we decide for the class 2-TWs of non-linear tree transducers with output alphabet $B^*$ whether or not the output language is balanced. △ Less

Submitted 13 March, 2020; v1 submitted 29 November, 2019; originally announced November 2019.

Comments: Major changes in Section 3 Balancedness of 2-TWs: instead of proving equivalence of LTWs over the involutive monoid we use the result that equivalence of LTWs over the free group is decidable in polynomial time (arXiv:2001.03480). A short version will be published in the conference proceedings of DLT 2020

How to Win First-Order Safety Games

Authors: Helmut Seidl, Christian Müller, Bernd Finkbeiner

Abstract: First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Desirable properties of these systems such as functional correctness or noninterference have conveniently been formulated as safety properties. In order to automatically syn… ▽ More First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Desirable properties of these systems such as functional correctness or noninterference have conveniently been formulated as safety properties. In order to automatically synthesize strategies that enforce safety or noninterference, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is in fact, equivalent to second-order quantifier elimination. For the important case of FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of noninterference properties. Based on general techniques for second-order quantifier elimination, we provide abstraction and refinement techniques in order to synthesize FO strategies that enforce safety. We demonstrate the usefulness of our approach by inferring nontrivial FO specifications in a leader election protocol as well as for paper assignment in a conference mangagement system to exclude unappreciated disclosure of reports. △ Less

Submitted 13 November, 2019; v1 submitted 16 August, 2019; originally announced August 2019.

ACM Class: F.4

Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time

Authors: Helmut Seidl, Raphaela Palenta, Sebastian Maneth

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 pro… ▽ More 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. △ Less

Submitted 11 February, 2019; originally announced February 2019.

Verifying Security Policies in Multi-agent Workflows with Loops

Authors: Bernd Finkbeiner, Christian Müller, Helmut Seidl, Eugen Zălinescu

Abstract: 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 pro… ▽ More 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. △ Less

Submitted 29 August, 2017; originally announced August 2017.

Comments: Authors' version of the corresponding CCS 2017 conference paper

Computing the longest common prefix of a context-free language in polynomial time

Authors: Michael Luttenberger, Raphaela Palenta, Helmut Seidl

Abstract: 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… ▽ More 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. △ Less

Submitted 6 January, 2018; v1 submitted 22 February, 2017; originally announced February 2017.

ACM Class: F.4.3

Reachability for dynamic parametric processes

Authors: Anca Muscholl, Helmut Seidl, Igor Walukiewicz

Abstract: In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems,… ▽ More In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME. △ Less

Submitted 17 September, 2016; originally announced September 2016.

Comments: 31 pages

ACM Class: D.2.4; F.3.1

Enforcing Termination of Interprocedural Analysis

Authors: Stefan Schulze Frielinghaus, Helmut Seidl, Ralf Vogler

Abstract: Interprocedural analysis by means of partial tabulation of summary functions may not terminate when the same procedure is analyzed for infinitely many abstract calling contexts or when the abstract domain has infinite strictly ascending chains. As a remedy, we present a novel local solver for general abstract equation systems, be they monotonic or not, and prove that this solver fails to terminate… ▽ More Interprocedural analysis by means of partial tabulation of summary functions may not terminate when the same procedure is analyzed for infinitely many abstract calling contexts or when the abstract domain has infinite strictly ascending chains. As a remedy, we present a novel local solver for general abstract equation systems, be they monotonic or not, and prove that this solver fails to terminate only when infinitely many variables are encountered. We clarify in which sense the computed results are sound. Moreover, we show that interprocedural analysis performed by this novel local solver, is guaranteed to terminate for all non-recursive programs --- irrespective of whether the complete lattice is infinite or has infinite strictly ascending or descending chains. △ Less

Submitted 24 June, 2016; originally announced June 2016.

Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable

Authors: Helmut Seidl, Sebastian Maneth, Gregor Kemper

Abstract: 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… ▽ More 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. Furthermore, we extend our result to deterministic top-down tree-to-string transducers which produce output not in a free monoid but in a free group. △ Less

Submitted 27 January, 2017; v1 submitted 31 March, 2015; originally announced March 2015.

Efficiently intertwining widening and narrowing

Authors: Gianluca Amato, Francesca Scozzari, Helmut Seidl, Kalmer Apinis, Vesal Vojdani

Abstract: Non-trivial analysis problems require posets 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. The strict separation into phases, however, may unnecessarily give up precision that cannot be recovered later, a… ▽ More Non-trivial analysis problems require posets 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. The strict separation into phases, however, may unnecessarily give up precision that cannot be recovered later, as over-approximated interim results have to be fully propagated through the equation the system. Additionally, classical two-phased approach is not suitable for equation systems with infinitely many unknowns---where demand driven solving must be used. Construction of an intertwined approach must be able to answer when it is safe to apply narrowing---or when widening must be applied. In general, this is a difficult problem. In case the right-hand sides of equations are monotonic, however, we can always apply narrowing whenever we have reached a post-fixpoint for an equation. The assumption of monotonicity, though, is not met in presence of widening. It is also not met by equation systems corresponding to context-sensitive inter-procedural analysis, possibly combining context-sensitive analysis of local information with flow-insensitive analysis of globals. As a remedy, we present a novel operator that combines a given widening operator with a given narrowing operator. We present adapted versions of round-robin as well as of worklist iteration, local and side-effecting solving algorithms for the combined operator and prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns (constraint variables) are encountered. Practical remedies are proposed for termination in the non-monotonic case. △ Less

Submitted 3 March, 2015; originally announced March 2015.

Comments: For submission to Science of Computer Programming

Inter-procedural Two-Variable Herbrand Equalities

Authors: Stefan Schulze Frielinghaus, Michael Petter, Helmut Seidl

Abstract: We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments whose right-hand sides depend on at most one variable are taken into account. The analysis is based on procedure summaries representing the weakest pre-conditions for finitely many generic post-conditions with template variables. In order to arrive at effective representations for all… ▽ More We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments whose right-hand sides depend on at most one variable are taken into account. The analysis is based on procedure summaries representing the weakest pre-conditions for finitely many generic post-conditions with template variables. In order to arrive at effective representations for all occurring weakest pre-conditions, we show for almost all values possibly computed at run-time, that they can be uniquely factorized into tree patterns and a ground term. Moreover, we introduce an approximate notion of subsumption which is effectively decidable and ensures that finite conjunctions of equalities may not grow infinitely. Based on these technical results, we realize an effective fixpoint iteration to infer all inter-procedurally valid Herbrand equalities for these programs. Finally we show that an invariant candidate with a constant number of variables, can be verified in polynomial time. △ Less

Submitted 10 May, 2017; v1 submitted 16 October, 2014; originally announced October 2014.

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 2 (May 12, 2017) lmcs:3655

Parametric Strategy Iteration

Authors: Thomas M. Gawlitza, Martin D. Schwarz, Helmut Seidl

Abstract: Program behavior may depend on parameters, which are either configured before compilation time, or provided at run-time, e.g., by sensors or other input devices. Parametric program analysis explores how different parameter settings may affect the program behavior. In order to infer invariants depending on parameters, we introduce parametric strategy iteration. This algorithm determines the preci… ▽ More Program behavior may depend on parameters, which are either configured before compilation time, or provided at run-time, e.g., by sensors or other input devices. Parametric program analysis explores how different parameter settings may affect the program behavior. In order to infer invariants depending on parameters, we introduce parametric strategy iteration. This algorithm determines the precise least solution of systems of integer equations depending on surplus parameters. Conceptually, our algorithm performs ordinary strategy iteration on the given integer system for all possible parameter settings in parallel. This is made possible by means of region trees to represent the occurring piecewise affine functions. We indicate that each required operation on these trees is polynomial-time if only constantly many parameters are involved. Parametric strategy iteration for systems of integer equations allows to construct parametric integer interval analysis as well as parametric analysis of differences of integer variables. It thus provides a general technique to realize precise parametric program analysis if numerical properties of integer variables are of concern. △ Less

Submitted 19 June, 2014; originally announced June 2014.

Look-Ahead Removal for Top-Down Tree Transducers

Authors: Joost Engelfriet, Sebastian Maneth, Helmut Seidl

Abstract: Top-down tree transducers are a convenient formalism for describing tree transformations. They can be equipped with regular look-ahead, which allows them to inspect a subtree before processing it. In certain cases, such a look-ahead can be avoided and the transformation can be realized by a transducer without look-ahead. Removing the look-ahead from a transducer, if possible, is technically highly… ▽ More Top-down tree transducers are a convenient formalism for describing tree transformations. They can be equipped with regular look-ahead, which allows them to inspect a subtree before processing it. In certain cases, such a look-ahead can be avoided and the transformation can be realized by a transducer without look-ahead. Removing the look-ahead from a transducer, if possible, is technically highly challenging. For a restricted class of transducers with look-ahead, namely those that are total, deterministic, ultralinear, and bounded erasing, we present an algorithm that, for a given transducer from that class, (1) decides whether it is equivalent to a total deterministic transducer without look-ahead, and (2) constructs such a transducer if the answer is positive. For the whole class of total deterministic transducers with look-ahead we present a similar algorithm, which assumes that a so-called difference bound is known for the given transducer. The designer of a transducer can usually also determine a difference bound for it. △ Less

Submitted 2 December, 2015; v1 submitted 11 November, 2013; originally announced November 2013.

Comments: 57 pages, to appear in TCS

MSC Class: 68Q05; 68Q45 ACM Class: F.1.1; F.4.3

Numerical Invariants through Convex Relaxation and Max-Strategy Iteration

Authors: Thomas Martin Gawlitza, Helmut Seidl

Abstract: In this article we develop a max-strategy improvement algorithm for computing least fixpoints of operators on on the reals that are point-wise maxima of finitely many monotone and order-concave operators. Computing the uniquely determined least fixpoint of such operators is a problem that occurs frequently in the context of numerical program/systems verification/analysis. As an example for an appl… ▽ More In this article we develop a max-strategy improvement algorithm for computing least fixpoints of operators on on the reals that are point-wise maxima of finitely many monotone and order-concave operators. Computing the uniquely determined least fixpoint of such operators is a problem that occurs frequently in the context of numerical program/systems verification/analysis. As an example for an application we discuss how our algorithm can be applied to compute numerical invariants of programs by abstract interpretation based on quadratic templates. △ Less

Submitted 5 April, 2012; originally announced April 2012.

Comments: 42 pages, conference version appears in the proceedings of the Static Analysis Symposium 2010

ACM Class: F.3.2

Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying

Authors: Helmut Seidl, Kumar Neeraj Verma

Abstract: Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class $\mathcal 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… ▽ More Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class $\mathcal 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. △ Less

Submitted 3 November, 2005; originally announced November 2005.

Comments: Long version of paper presented at LPAR 2004