RTA on Saturday, August 12th

FLoC Opening and Plenary Session (08:45‑10:00)
Chair: Moshe Vardi, Thomas Ball, Wolfram Schulte, Rajeev Alur
Location: Grand Ballroom C

08:45‑09:00

Introduction and Welcome

09:00‑10:00

Randal E. Bryant (Carnegie Mellon University) Formal Verification of Infinite State Systems using Boolean Methods [ppt] Most successful automated formal verification tools are based on a bit-level model of computation. Using powerful inference engines, such as Binary Decision Diagrams (BDDs) and Boolean satisfiability (SAT) checkers, symbolic model checkers and similar tools can analyze all possible behaviors of very large, finite-state systems. For many hardware and software systems, we would like to go beyond bit-level models to handle systems that are truly infinite state, or that are better modeled as infinite-state systems. Examples include programs manipulating integer data, concurrency protocols involving arbitrary numbers of processes, and systems containing buffers where the sizes are described parametrically. Historically, much of the effort in verifying such systems involved automated theorem provers, requiring considerable guidance and expertise on the part of the user. We would like to devise approaches for these more powerful computational models that retain the desirable features of model checking, such as the high degree of automation and the ability to generate counterexamples. We have developed UCLID, a prototype verifier for infinite-state systems. The UCLID modeling language extends that of SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is quite expressive, yet it still permits a decision procedure that transforms the formula into propositional logic and then uses a SAT solver. UCLID supports multiple forms of verification, requiring different levels of sophistication in the handling of quantifiers. We demonstrate UCLID's modeling and verification capabilities with such examples as out-of-order microprocessors and directory-based cache coherency protocols.

Break (10:00‑10:30)

Session 1: Constraints and Optimization (10:30‑12:30)
Chair: Denis Lugiez
Location: Willow A/B

10:30‑11:00	Michael Codish (Ben-Gurion University) Vitaly Lagoon (University of Melbourne) Peter Stuckey (Melbourne University) Solving Partial Order Constraints for LPO Termination This paper introduces a new kind of propositional encoding for reasoning about partial orders. The symbols in an unspecified partial order are viewed as variables which take integer values and are interpreted as indices in the order. % For a partial order statement on $n$ symbols each index is represented in $\lceil\log_2 n\rceil$ propositional variables and partial order constraints between symbols are modeled on the bit representations. % We illustrate the application of our approach to determine LPO termination for term rewrite systems. Experimental results are unequivocal, indicating orders of magnitude speedups in comparison with current implementations for LPO termination. % The proposed encoding is general and relevant to other applications which involve propositional reasoning about partial orders.
11:00‑11:30	Traian Serbanuta (UIUC) Grigore Rosu (University of Illinois at Urbana-Champaign) Computationally Equivalent Elimination of Conditions An automatic and easy to implement transformation of conditional term rewrite systems into computationally equivalent unconditional term rewrite systems is presented. No special support is needed from the underlying unconditional rewrite engine. Since unconditional rewriting is more amenable to parallelization, our transformation is expected to lead to efficient concurrent implementations of rewriting.
11:30‑12:00	Sergio Antoy (Portland State University) Daniel Brown (Portland State University) Su-Hui Chiang (Portland State University) On the Correctness of Bubbling Bubbling, a recently introduced graph transformation for functional logic computations, is well-suited for the reduction of redexes with distinct replacements. Unlike backtracking, bubbling preserves operational completeness; unlike copying, it avoids the up-front construction of large contexts of redexes, an expensive and frequently wasteful operation. We recall the notion of bubbling and offer the first proof of its completeness and soundness with respect to rewriting.
12:00‑12:30	Joe Hendrix (University of Illinois at Urbana-Champaign) Hitoshi Ohsaki (National Institute of Advanced Industrial Science and Technology) Mahesh Viswanathan (University of Illinois, Urbana-Champaign) Propositional Tree Automata In the paper we introduce a new tree-automata framework, called propositional tree automata, capturing the class of tree languages that are closed under equational theory and Boolean operations. This framework originated in work on developing a sufficient completeness checker for specifications with associative and/or commutative operators. Unlike regular equational tree automata, propositional tree automata are guaranteed to be closed under Boolean operations via very simple algorithms. This extra power does not affect the decidability of the membership problem relative to equational tree automata. We then explore the emptiness problem for propositional tree automata over associative theories in particular detail. Though testing emptiness is not computable in general for this class, we present an approach based on techniques from machine learning that can be used to show the emptiness in practice.

Lunch break (12:30‑14:00)

Session 2: Equational Reasoning (14:00‑15:30)
Chair: Franz Baader
Location: Willow A/B

14:00‑14:30	Bernhard Gramlich (technische universitaet wien) Salvador Lucas (DSIC, Universidad Politécnica de Valencia) Generalizing Newman's Lemma for Left-Linear Rewrite Systems Confluence criteria for non-terminating rewrite systems are known to be rare and notoriously difficult to obtain. Here we prove a new result in this direction. Our main result is a generalized version of Newman's Lemma for left-linear term rewriting systems that does not need a full termination assumption. We discuss its relationships to previous confluence criteria, its restrictions, examples of application as well as open problems. The whole approach is developed in the (more general) framework of context-sensitive rewriting which thus turns out to be useful also for ordinary (context-free) rewriting.
14:30‑15:00	Piotr Hoffman (Warsaw University) Unions of Equational Monadic Theories We investigate the decidability of unions of decidable equational theories. We focus on monadic theories, i.e., theories over signatures with unary symbols only. This allows us to make use of the equivalence between monoid amalgams and unions of monadic theories. We show that if the intersection theory is unitary, then the decidability of the union is guaranteed by the decidability of tensor products. We prove that if the intersection theory is a group or a group with zero, then the union is decidable. Finally, we show that even if the intersection theory is a 3-element monoid and is unitary, the union may be undecidable, but that it will always be decidable for 2-element unitary monoids. We also show that unions of regular theories, i.e., theories recognizable by finite automata, can be undecidable. However, we prove that they are decidable if the intersection theory is unitary.
15:00‑15:30	Jean-Pierre Jouannaud (École Polytechnique) Modular Church-Rosser Modulo In 1987, Toyama proved that the union of two confluent term-rewriting systems that share absolutely no function symbols or constants is likewise confluent, a property called modularity. The proof of this beautiful modularity result, technically based on slicing terms into an homogeneous cap and a so called alien, possibly heterogeneous substitution, was later substantially simplified by Klop, Middledorp, de Vrijer and Toyama. In this paper we present a further simplification of the proof of Toyama's result for confluence, which shows that the crux of the problem lies in two different properties: a cleaning lemma, whose goal is to anticipate the application of collapsing reductions; a modularity property of ordered completion, that allows to pairwise match the caps and alien substitutions of two equivalent terms. We then show that Toyama's modularity result scales up to rewriting modulo equations in all cases.

Break (15:30‑16:00)

Session 3: System Verification (16:00‑17:00)
Chair: Ralf Treinen
Location: Willow A/B

16:00‑16:30

Yannick Chevalier (IRIT) Michael Rusinowitch (LORIA) Hierarchical Combination of Intruder Theories Recently rewriting techniques have proved to be very effective for detecting attack on cryptographic protocols. These analysis can be improved, for finding more subtle weaknesses, by a more accurate modelling of operators employed by protocols. Several works have shown how to handle a single algebraic operator (associated with a fixed intruder theory) or how to combine several operators satisfying disjoint theories. However several interesting equational theories, like exponentiation with an abelian group law for exponents remains out of the scope of these techniques. This has motivated us to introduce a new notion of hierarchical combination for intruder theories and to prove decidability results for the deduction problem

16:30‑17:00

Yohan Boichut (LIFC - University of Franche Comte) Thomas Genet (IRISA - university of Rennes) Feasible Trace Reconstruction for Rewriting Approximations Term Rewriting Systems are now commonly used as a modeling language for programs or systems. On those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. For disproving reachability (i.e. proving non reachability of a term) on non terminating and non confluent rewriting models, Knuth-Bendix completion and other usual rewriting techniques do not apply. Using the tree automaton completion technique, it has been shown that the non reachability of a term t can be shown by computing an over-approximation of the set of reachable terms and prove that t is not in the approximation. However, when the term t is in the approximation, nothing can be said. In this paper, we refine this approach and propose a method taking advantage of the approximation to compute a rewriting path to the reachable term when it exists. This algorithm has been prototyped in the Timbuk tool. We present some experiments with this prototype showing the efficiency and the interest of such an approach w.r.t. verification of rewriting models.

RTA Business Meeting (17:00‑18:00)
Location: Willow A/B