Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 11th International Conference on Language and Automata Theory and Applications, LATA 2017, held in Umeå, Sweden, in March 2017.

The 31 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 73 submissions. The papers cover the following topics: algorithmic learning and semantics; automata and logics; combinatorics on words, compression, and pattern matching; complexity; finite automata; grammars, languages, and parsing; graphs and Petri Nets; non-classical automata; and pushdown automata and systems.

Inhaltsverzeichnis

Frontmatter

Invited Talks

Frontmatter

Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in

Recently introduced approaches for relaxed query answering, approximately defining concepts, and approximately solving unification problems in Description Logics have in common that they are based on the use of concept comparison measures together with a threshold construction. In this paper, we will briefly review these approaches, and then show how weighted automata working on infinite trees can be used to construct computable concept comparison measures for $$\mathcal {FL}_0$$ that are equivalence invariant w.r.t. general TBoxes. This is a first step towards employing such measures in the mentioned approximation approaches.

Franz Baader, Oliver Fernández Gil, Pavlos Marantidis

Logic, Languages, and Rules for Web Data Extraction and Reasoning over Data

This paper gives a short overview of specific logical approaches to data extraction, data management, and reasoning about data. In particular, we survey theoretical results and formalisms that have been obtained and used in the context of the Lixto Project at TU Wien, the DIADEM project at the University of Oxford, and the VADA project, which is currently being carried out jointly by the universities of Edinburgh, Manchester, and Oxford. We start with a formal approach to web data extraction rooted in monadic second order logic and monadic Datalog, which gave rise to the Lixto data extraction system. We then present some complexity results for monadic Datalog over trees and for XPath query evaluation. We further argue that for value creation and for ontological reasoning over data, we need existential quantifiers (or Skolem terms) in rule heads, and introduce the Datalog$$^\pm $$ family. We give an overview of important members of this family and discuss related complexity issues.

Georg Gottlob, Christoph Koch, Andreas Pieris

Algorithmic Learning and Semantics

Frontmatter

A Stable Non-interleaving Early Operational Semantics for the Pi-Calculus

We give the first non-interleaving early operational semantics for the pi-calculus which generalizes the standard interleaving semantics and unfolds to the stable model of prime event structures. Our starting point is the non-interleaving semantics given for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject) causality and events are defined from a notion of locations derived from the syntactic structure of the process terms. The semantics is conservatively extended with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the dynamic communication topology of the pi-calculus. We prove that the semantics generalises both the standard interleaving early semantics for the pi-calculus and the non-interleaving semantics for CCS. In particular, it gives rise to a labelled asynchronous transition system unfolding to prime event structures.

Thomas Troels Hildebrandt, Christian Johansen, Håkon Normann

Efficient Learning of Tier-Based Strictly k-Local Languages

We introduce an algorithm that learns the class of Tier-based Strictly k-Local (TSL$$_k$$) formal languages in polynomial time on a sample of positive data whose size is bounded by a constant. The TSL$$_k$$ languages are useful in modeling the cognition of sound patterns in natural language [6, 11], and it is known that they can be efficiently learned from positive data in the case that $$k=2$$ [9]. We extend this result to any k and improve on its time efficiency. We also refine the definition of a canonical TSL$$_k$$ grammar and prove several properties about these grammars that aid in their learning.

Adam Jardine, Kevin McMullin

The Strong, Weak, and Very Weak Finite Context and Kernel Properties

We identify the properties of context-free grammars that exactly correspond to the behavior of the dual and primal versions of Clark and Yoshinaka’s distributional learning algorithm and call them the very weak finite context/kernel property. We show that the very weak finite context property does not imply Yoshinaka’s weak finite context property, which has been assumed to hold of the target language for the dual algorithm to succeed. We also show that the weak finite context property is genuinely weaker than Clark’s strong finite context property, settling a question raised by Yoshinaka.

Makoto Kanazawa, Ryo Yoshinaka

Automata and Logics

Frontmatter

-Memory Automata over the Alphabet

The concept of $$\mathbb {N}$$-memory automaton over the alphabet $$\mathbb {N}$$ is studied. We show a result on robustness of this model (by a connection to MSO-logic), give a discussion on its expressive power and closure properties, and show among other decidability results the solvability of the non-emptiness problem. We conclude with perspectives for applications and some open questions.

Benedikt Brütsch, Patrick Landwehr, Wolfgang Thomas

An Automata View to Goal-Directed Methods

Consequence-based and automata-based algorithms encompass two families of approaches that have been thoroughly studied as reasoning methods for many logical formalisms. While automata are useful for finding tight complexity bounds, consequence-based algorithms are typically simpler to describe, implement, and optimize. In this paper, we show that consequence-based reasoning can be reduced to the emptiness test of an appropriately built automaton. Thanks to this reduction, one can focus on developing efficient consequence-based algorithms, obtaining complexity bounds and other benefits of automata methods for free.

Lisa Hutschenreiter, Rafael Peñaloza

A Calculus of Cyber-Physical Systems

We propose a hybrid process calculus for modelling and reasoning on cyber-physical systems (CPSs). The dynamics of the calculus is expressed in terms of a labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based behavioural semantics which support compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial case study.

Ruggero Lanotte, Massimo Merro

Combinatorics on Words, Compression, and Pattern Matching

Frontmatter

Efficient Pattern Matching in Elastic-Degenerate Texts

Motivated by applications in bioinformatics, in what follows, we extend the notion of gapped strings to elastic-degenerate strings. An elastic-degenerate string can been seen as an ordered collection of solid (standard) strings interleaved by elastic-degenerate symbols; each such symbol corresponds to a set of two or more variable-length solid strings. In this article, we present an algorithm for solving the pattern matching problem with a solid pattern and an elastic-degenerate text running in $$\mathcal {O}(N+\alpha \gamma mn)$$ time; where m is the length of the pattern; n and N are the length and total size of the elastic-degenerate text, respectively; $$\alpha $$ and $$\gamma $$ are parameters, respectively representing the maximum number of strings in any elastic-degenerate symbol of the text and the maximum number of elastic-degenerate symbols spanned by any occurrence of the pattern in the text. The space used by the proposed algorithm is $$\mathcal {O}(N)$$.

Costas S. Iliopoulos, Ritu Kundu, Solon P. Pissis

Integrated Encryption in Dynamic Arithmetic Compression

A compression cryptosystem based on adaptive arithmetic coding is proposed, in which the updates of the frequency tables for the underlying alphabet are done selectively, according to some secret key K. We give empirical evidence that the compression performance is not hurt, and discuss also aspects of the system being used as an encryption method.

Shmuel T. Klein, Dana Shapira

Two-Dimensional Palindromes and Their Properties

A two-dimensional word (2D) is a rectangular finite array of letters from the alphabet $$\varSigma $$. A 2D word is said to be a 2D palindrome if it is equal to its reverse image. In this paper, we study some combinatorial properties of 2D palindromes. In particular, we provide a sufficient condition under which a 2D word is said to be a 2D palindrome, discuss the necessary and sufficient condition under which a 2D word can be decomposed into 2D palindromes, and find the relation between the set of all 2D palindromes and the set of all 2D primitive words. We also show that the set of all 2D palindromes is not a recognizable language, and study a special class of 2D palindromes, namely 2D palindrome square words.

Manasi S. Kulkarni, Kalpana Mahalingam

Complexity

Frontmatter

Complexity of Left-Ideal, Suffix-Closed and Suffix-Free Regular Languages

A language L over an alphabet $$\varSigma $$ is suffix-convex if, for any words $$x,y,z\in \varSigma ^*$$, whenever z and xyz are in L, then so is yz. Suffix-convex languages include three special cases: left-ideal, suffix-closed, and suffix-free languages. We examine complexity properties of these three special classes of suffix-convex regular languages. In particular, we study the quotient/state complexity of boolean operations, product (concatenation), star, and reversal on these languages, as well as the size of their syntactic semigroups, and the quotient complexity of their atoms.

Janusz A. Brzozowski, Corwin Sinnamon

On the Complexity of Hard Enumeration Problems

Complexity theory provides a wealth of complexity classes for analyzing the complexity of decision and counting problems. Despite the practical relevance of enumeration problems, the tools provided by complexity theory for this important class of problems are very limited. In particular, complexity classes analogous to the polynomial hierarchy and an appropriate notion of problem reduction are missing. In this work, we lay the foundations for a complexity theory of hard enumeration problems by proposing a hierarchy of complexity classes and by investigating notions of reductions for enumeration problems.

Nadia Creignou, Markus Kröll, Reinhard Pichler, Sebastian Skritek, Heribert Vollmer

Consensus String Problem for Multiple Regular Languages

The consensus string (or center string, closest string) of a set S of strings is defined as a string which is within a radius r from all strings in S. It is well-known that the consensus string problem for a finite set of equal-length strings is NP-complete. We study the consensus string problem for multiple regular languages. We define the consensus string of languages $$L_1, \ldots , L_k$$ to be within distance at most r to some string in each of the languages $$L_1, \ldots , L_k$$. We also study the complexity of some parameterized variants of the consensus string problem. For a constant k, we give a polynomial time algorithm for the consensus string problem for k regular languages using additive weighted finite automata. We show that the consensus string problem for multiple regular languages becomes intractable when k is not fixed. We also examine the case when the length of the consensus string is given as part of input.

Yo-Sub Han, Sang-Ki Ko, Timothy Ng, Kai Salomaa

The Weight in Enumeration

In our setting enumeration amounts to generate all solutions of a problem instance without duplicates. We address the problem of enumerating the models of B-formulæ. A B-formula is a propositional formula whose connectives are taken from a fixed set B of Boolean connectives. Without imposing any specific order to output the solutions, this task is solved. We completely classify the complexity of this enumeration task for all possible sets of connectives B imposing the orders of (1) non-decreasing weight, (2) non-increasing weight; the weight of a model being the number of variables assigned to 1. We consider also the weighted variants where a non-negative integer weight is assigned to each variable and show that this add-on leads to more sophisticated enumeration algorithms and even renders previously tractable cases intractable, contrarily to the constraint setting. As a by-product we obtain also complexity classifications for the optimization problems known as $$\textsc {Min}\hbox {-}\textsc {Ones}$$ and $$\textsc {Max}\hbox {-}\textsc {Ones}$$ which are in the B-formula setting two different tasks.

Johannes Schmidt

Finite Automata

Frontmatter

Minimization of Finite State Automata Through Partition Aggregation

We present a minimization algorithm for finite state automata that finds and merges bisimulation-equivalent states, identified through partition aggregation. We show the algorithm to be correct and run in time $$ O \left( n^2 d^2 \left| \Sigma \right| \right) $$, where n is the number of states of the input automaton $$M$$, d is the maximal outdegree in the transition graph for any combination of state and input symbol, and $$\left| \Sigma \right| $$ is the size of the input alphabet. The algorithm is slower than those based on partition refinement, but has the advantage that intermediate solutions are also language equivalent to $$M$$. As a result, the algorithm can be interrupted or put on hold as needed, and the derived automaton is still useful. Furthermore, the algorithm essentially searches for the maximal model of a characteristic formula for $$M$$, so many of the optimisation techniques used to gain efficiency in SAT solvers are likely to apply.

Johanna Björklund, Loek Cleophas

Derivatives and Finite Automata of Expressions in Star Normal Form

This paper studies derivatives and automata for expressions in star normal form as defined by Brüggemann-Klein. For an expression in star normal form, the paper shows that the derivatives are either $$\emptyset $$ or unique, while in general Berry and Sethi’s result shows the derivatives are either $$\emptyset $$ or similar. It is known that the partial derivative automaton and the follow automaton are two small automata, each of which is a quotient of the position automaton. For the relation between the partial derivative and follow automata, however, Ilie and Yu stated that a rigorous analysis is necessary but difficult. The paper tackles the issue, and presents several results. Our work shows that there are different conditions under which the relation of the two automata can be different.

Haiming Chen, Ping Lu

Finding DFAs with Maximal Shortest Synchronizing Word Length

It was conjectured by Černý in 1964 that a synchronizing DFA on n states always has a shortest synchronizing word of length at most $$(n-1)^2$$, and he gave a sequence of DFAs for which this bound is reached. In 2006 Trahtman conjectured that apart from Černý’s sequence only 8 DFAs exist attaining the bound. He gave an investigation of all DFAs up to certain size for which the bound is reached, and which do not contain other synchronizing DFAs. Here we extend this analysis in two ways: we drop this latter condition, and we drop limits on alphabet size. For $$n \le 4$$ we do the full analysis yielding 19 new DFAs with smallest synchronizing word length $$(n-1)^2$$, refuting Trahtman’s conjecture. All these new DFAs are extensions of DFAs that were known before. For $$n \ge 5$$ we prove that none of the DFAs in Trahtman’s analysis can be extended similarly. In particular, as a main result we prove that the Černý examples $$C_n$$ do not admit non-trivial extensions keeping the same smallest synchronizing word length $$(n-1)^2$$.

Henk Don, Hans Zantema

Lower Bound Methods for the Size of Nondeterministic Finite Automata Revisited

We revisit the following lower bound methods for the size of a nondeterministic finite automaton: the fooling set technique, the extended fooling set technique, and the biclique edge cover technique, presenting these methods in terms of quotients and atoms of regular languages. Although the lower bounds obtained by these methods are not necessarily tight, some classes of languages for which tight bounds can be achieved, are known. We show that languages with maximal reversal complexity belong to the class of languages for which the fooling set technique provides a tight bound. We also show that the extended fooling set technique is tight for a subclass of unary cyclic languages.

Hellis Tamm, Brink van der Merwe

Grammars, Languages, and Parsing

Frontmatter

Linear Parsing Expression Grammars

PEGs were formalized by Ford in 2004, and have several pragmatic operators (such as ordered choice and unlimited lookahead) for better expressing modern programming language syntax. Since these operators are not explicitly defined in the classic formal language theory, it is significant and still challenging to argue PEGs’ expressiveness in the context of formal language theory. Since PEGs are relatively new, there are several unsolved problems. One of the problems is revealing a subclass of PEGs that is equivalent to DFAs. This allows application of some techniques from the theory of regular grammar to PEGs. In this paper, we define Linear PEGs (LPEGs), a subclass of PEGs that is equivalent to DFAs. Surprisingly, LPEGs are formalized by only excluding some patterns of recursive nonterminal in PEGs, and include the full set of ordered choice, unlimited lookahead, and greedy repetition, which are characteristic of PEGs. Although the conversion judgement of parsing expressions into DFAs is undecidable in general, the formalism of LPEGs allows for a syntactical judgement of parsing expressions.

Nariyoshi Chida, Kimio Kuramitsu

On Finite-Index Indexed Grammars and Their Restrictions

The family, $${\mathsf{{\mathcal {L}}(IND_{LIN})}}$$, of languages generated by linear indexed grammars has been studied in the literature. It is known that the Parikh image of every language in $${\mathsf{{\mathcal {L}}(IND_{LIN})}}$$ is semi-linear. However, there are bounded semi-linear languages that are not in $${\mathsf{{\mathcal {L}}(IND_{LIN})}}$$. Here, we look at larger families of (restricted) indexed languages and study their properties, their relationships, and their decidability properties.

Flavio D’Alessandro, Oscar H. Ibarra, Ian McQuillan

A Derivational Model of Discontinuous Parsing

The notion of latent-variable probabilistic context-free derivation of syntactic structures is enhanced to allow heads and unrestricted discontinuities. The chosen formalization covers both constituent parsing and dependency parsing. The derivational model is accompanied by an equivalent probabilistic automaton model. By the new framework, one obtains a probability distribution over the space of all discontinuous parses. This lends itself to intrinsic evaluation in terms of perplexity, as shown in experiments.

Mark-Jan Nederhof, Anssi Yli-Jyrä

Cut Languages in Rational Bases

We introduce a so-called cut language which contains the representations of numbers in a rational base that are less than a given threshold. The cut languages can be used to refine the analysis of neural net models between integer and rational weights. We prove a necessary and sufficient condition when a cut language is regular, which is based on the concept of a quasi-periodic power series. For a nonnegative base and digits, we achieve a dichotomy that a cut language is either regular or non-context-free while examples of regular and non-context-free cut languages are presented. We show that any cut language with a rational threshold is context-sensitive.

Jiří Šíma, Petr Savický

Graphs and Petri Nets

Frontmatter

Merging Relations: A Way to Compact Petri Nets’ Behaviors Uniformly

Compacting Petri nets behaviors means to develop a more succinct representation of all the possible executions of a net, still giving the capability to reason on properties fulfilled by the computations of the net. To do so suitable equivalences on alternative executions have to be engineered. We introduce a general notion of merging relation covering the existing approaches to compact behaviors and we discuss how to enforce that the more succinct net is an unravel net, namely a net where dependencies can be identified (almost) syntactically.

Giovanni Casu, G. Michele Pinna

Partitioning Graphs into Induced Subgraphs

We study the Partition into$$H$$ problem from the parametrized complexity point of view. In the Partition into$$H$$ problem the task is to partition the vertices of a graph G into sets $$V_1,\dots ,V_r$$ such that the graph H is isomorphic to the subgraph of G induced by each set $$V_i$$ for $$i = 1,\dots ,r.$$ The pattern graph H is fixed.For the parametrization we consider three distinct structural parameters of the graph G – namely the tree-width, the neighborhood diversity, and the modular-width. For the parametrization by the neighborhood diversity we obtain an FPT algorithm for every graph H. For the parametrization by the tree-width we obtain an FPT algorithm for every connected graph H. Thus resolving an open question of Gajarský et al. from IPEC 2013 [9]. Finally, for the parametrization by the modular-width we derive an FPT algorithm for every prime graph H.

Dušan Knop

Space Complexity of Reachability Testing in Labelled Graphs

Fix an algebraic structure $$(\mathcal {A}, *)$$. Given a graph $$G =(V, E)$$ and the labelling function $$\phi $$ ($$\phi : E \rightarrow \mathcal {A}$$) for the edges, two nodes s, $$t \in V$$, and a subset $$F \subseteq \mathcal {A}$$, the $$\mathcal {A}$$-Reach problem asks if there is a path p (need not be simple) from s to t whose yield (result of the operation in the ordered set of the labels of the edges constituting the path) is in F. On the complexity frontier of this problem, we show the following results.When $$\mathcal {A}$$ is a group whose size is polynomially bounded in the size of the graph (hence equivalently presented as a multiplication table at the input), and the graph is undirected, the $$\mathcal {A}$$-Reach problem is in $$\mathsf {L}$$. Building on this, using a decomposition in [4], we show that, when $$\mathcal {A}$$ is a fixed quasi-group, and the graph is undirected, the $$\mathcal {A}$$-Reach problem is in $$\mathsf {L}$$. In contrast, we show $$\mathsf {NL}$$-hardness of the problem over bidirected graphs, when $$\mathcal {A}$$ is a matrix group over $$\mathbb {Q}$$. When $$\mathcal {A}$$ is a fixed aperiodic monoid, we show that the problem is $$\mathsf {NL}$$-complete.As our main theorem, we prove a dichotomy for graphs labelled with fixed aperiodic monoids by showing that for every fixed aperiodic monoid $$\mathcal {A}$$, $$\mathcal {A}$$-Reach problem is either in $$\mathsf {L}$$ or is $$\mathsf {NL}$$-complete.We show that there exists a monoid M, such that the reachability problem in general DAGs can be reduced to $$\mathcal {A}$$-Reach problem for planar non-bipartite DAGs labelled with M. In contrast, we show that if the planar DAGs that we obtain above are bipartite, the problem can be further reduced to reachability testing in planar DAGs and hence is in $$\mathsf {UL}$$.

Vidhya Ramaswamy, Jayalal Sarma, K. S. Sunil

Non-classical Automata

Frontmatter

Most General Property-Preserving Updates

Systems need to be updated to last for a long time in a dynamic environment, and to cope with changing requirements. It is important for updates to preserve the desirable properties of the system under update, while possibly enforcing new ones.Here we consider a simple yet general update mechanism, which replaces a component of the system with a new one. The context, i.e., the rest of the system, remains unchanged. We define contexts and components as Constraint Automata interacting via either asynchronous or synchronous communication, and we express properties using Constraint Automata too. Then we build most general updates which preserve specific properties, considering both a single property and all the properties satisfied by the original system, in a given context or in all possible contexts.

Davide Bresolin, Ivan Lanese

Over Which Monoids is the Transducer Determinization Procedure Applicable?

The input determinization of a finite-state transducer for constructing an equivalent subsequential transducer is performed by the well-known inductive transducer determinization procedure. This procedure has been shown to complete for rational functions with the bounded variation property. The result has been obtained for functions $$f : \varSigma ^*\rightarrow \mathcal {M}$$, where $$\mathcal {M}$$ is a free monoid, the monoid of non-negative real numbers with addition or a Cartesian product of those monoids. In this paper we generalize this result and define and prove sufficient conditions for a monoid $$\mathcal {M}$$ and a rational function $$f : \varSigma ^*\rightarrow \mathcal {M}$$, under which the transducer determinization procedure is applicable and terminates.

Stefan Gerdjikov, Stoyan Mihov

Color War: Cellular Automata with Majority-Rule

Consider a graph $$G=(V,E)$$ and a random initial vertex-coloring such that each vertex is blue independently with probability $$p_{b}\le 1/2$$, and red otherwise. In each step, all vertices change their current color synchronously to the most frequent color in their neighborhood (in the case of a tie, a vertex conserves its current color). We are interested in the behavior of this very natural process, especially in 2-dimensional grids and tori (cellular automata with majority rule). In the present paper, as a main result we prove that a grid $$G_{n,n}$$ or a torus $$T_{n,n}$$ with 4-neighborhood (8-neighborhood) exhibits a threshold behavior: with high probability, it reaches a red monochromatic configuration in a constant number of steps if $$p_b\ll n^{-\frac{1}{2}}$$ ($$p_b\ll n^{-\frac{1}{6}}$$), but $$p_b\gg n^{-\frac{1}{2}}$$ ($$p_b\gg n^{-\frac{1}{6}}$$) results in a bichromatic period of configurations of length one or two, after at most $$2n^2$$ ($$4n^2$$) steps with high probability.

Bernd Gärtner, Ahad N. Zehmakan

On the Computational Power of Affine Automata

We investigate the computational power of affine automata (AfAs) introduced in [4]. In particular, we present a simpler proof for how to change the cutpoint for any affine language and a method how to reduce error in bounded error case. Moreover, we address to the question of [4] by showing that any affine language can be recognized by an AfA with certain limitation on the entries of affine states and transition matrices. Lastly, we present the first languages shown to be not recognized by AfAs with bounded-error.

Mika Hirvensalo, Etienne Moutot, Abuzer Yakaryılmaz

Pushdown Automata and Systems

Frontmatter

Detecting Useless Transitions in Pushdown Automata

Pushdown automata may contain transitions that are never used in any accepting run of the automaton. We present an algorithm for detecting such useless transitions. A finite automaton that captures the possible stack content during runs of the pushdown automaton, is first constructed in a forward procedure to determine which transitions are reachable, and then employed in a backward procedure to determine which of these transitions can lead to a final state. An implementation of the algorithm is shown to exhibit a favorable performance.

Dick Grune, Wan Fokkink, Evangelos Chatzikalymnios, Brinio Hond, Peter Rutgers

Hardness Results for Coverability Problem of Well-Structured Pushdown Systems

Well-Structured Pushdown Systems (WSPDSs) are pushdown systems extended with states and stack alphabet to be vectors, for modeling (restricted) recursive concurrent programs. It has been considered to be “very close to the border of undecidability”. In this paper, we prove some hardness results for the coverability problem of WSPDSs. We show that for WSPDS with three dimensional vectors as states and WSPDS with three dimensional vectors as stack alphabet, the coverability problem becomes Ackermann-hard.

Chunmiao Li, Xiaojuan Cai

Reachability Analysis of Pushdown Systems with an Upper Stack

Pushdown systems (PDSs) are a natural model for sequential programs, but they can fail to accurately represent the way an assembly stack actually operates. Indeed, one may want to access the part of the memory that is below the current stack or base pointer, hence the need for a model that keeps track of this part of the memory. To this end, we introduce pushdown systems with an upper stack (UPDSs), an extension of PDSs where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules. We prove that the sets of successors $$post^*$$ and predecessors $$pre^*$$ of a regular set of configurations of such a system are not always regular, but that $$post^*$$ is context-sensitive, so that we can decide whether a single configuration is forward reachable or not. In order to underapproximate $$pre^*$$ in a regular fashion, we consider a bounded-phase analysis of UPDSs, where a phase is a part of a run during which either push or pop rules are forbidden. We then present a method to overapproximate $$post^*$$ that relies on regular abstractions of runs of UPDSs. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent.

Adrien Pommellet, Marcio Diaz, Tayssir Touili

Backmatter

Weitere Informationen