Showing 1–23 of 23 results for author: Avanzini, M

Expectation-based Analysis of Higher-Order Quantum Programs

Authors: Martin Avanzini, Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux

Abstract: The paper extends the expectation transformer based analysis of higher-order probabilistic programs to the quantum higher-order setting. The quantum language we are considering can be seen as an extension of PCF, featuring unbounded recursion. The language admits classical and quantum data, as well as a tick operator to account for costs. Our quantum expectation transformer translates such program… ▽ More The paper extends the expectation transformer based analysis of higher-order probabilistic programs to the quantum higher-order setting. The quantum language we are considering can be seen as an extension of PCF, featuring unbounded recursion. The language admits classical and quantum data, as well as a tick operator to account for costs. Our quantum expectation transformer translates such programs into a functional, non-quantum language, enriched with a type and operations over so called cost-structures. By specializing the cost-structure, this methodology makes it possible to study several expectation based properties of quantum programs, such as average case cost, probabilities of events or expected values, in terms of the translated non-quantum programs, this way enabling classical reasoning techniques. As a show-case, we adapt a refinement type system, capable of reasoning on upper-bounds. △ Less

Submitted 25 April, 2025; originally announced April 2025.

Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version)

Authors: Davide Davoli, Martin Avanzini, Tamara Rezk

Abstract: The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax… ▽ More The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax Abadi et al.'s language assumptions while demonstrating that layout randomization offers a comparable safety guarantee in a system with memory separation. However, in practice, speculative execution and side-channels are recognized threats to layout randomization. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution, and introduce enforcement mechanisms that can guarantee speculative kernel safety for safe system calls in the Spectre era. We implement three suitable mechanisms and we evaluate their performance overhead on the Linux kernel. △ Less

Submitted 11 April, 2025; v1 submitted 27 November, 2024; originally announced November 2024.

Comments: arXiv admin note: substantial text overlap with arXiv:2406.07278

A quantitative probabilistic relational Hoare logic

Authors: Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire

Abstract: We introduce eRHL, a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-conditions take values in the extended non-negative reals. Thanks to its quantitative assertions, eRHL overcomes randomness alignment restrictions from prior logics, including PRHL, a popular relational program logic used to reas… ▽ More We introduce eRHL, a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-conditions take values in the extended non-negative reals. Thanks to its quantitative assertions, eRHL overcomes randomness alignment restrictions from prior logics, including PRHL, a popular relational program logic used to reason about security of cryptographic constructions, and apRHL, a variant of PRHL for differential privacy. As a result, eRHL is the first relational probabilistic program logic to be supported by non-trivial soundness and completeness results for all almost surely terminating programs. We show that eRHL is sound and complete with respect to program equivalence, statistical distance, and differential privacy. We also show that every PRHL judgment is valid iff it is provable in eRHL. We showcase the practical benefits of eRHL with examples that are beyond reach of PRHL and apRHL. △ Less

Submitted 8 January, 2025; v1 submitted 24 July, 2024; originally announced July 2024.

On Kernel's Safety in the Spectre Era (Extended Version)

Authors: Davide Davoli, Martin Avanzini, Tamara Rezk

Abstract: The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax… ▽ More The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax Abadi et al.'s language assumptions while demonstrating that layout randomization offers a comparable safety guarantee in a system with memory separation. However, in practice, speculative execution and side-channels are recognized threats to layout randomization. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution and introduce a new condition, that allows us to formally prove kernel safety in the Spectre era. Our research demonstrates that under this condition, the system remains safe without relying on layout randomization. We also demonstrate that our condition can be sensibly weakened, leading to enforcement mechanisms that can guarantee kernel safety for safe system calls in the Spectre era. △ Less

Submitted 11 April, 2025; v1 submitted 11 June, 2024; originally announced June 2024.

On the Hardness of Analyzing Quantum Programs Quantitatively

Authors: Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix

Abstract: In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express… ▽ More In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest precondition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction-a restriction to polynomials of bounded degree over a real closed field-we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method. △ Less

Submitted 21 December, 2023; originally announced December 2023.

Automated Expected Value Analysis of Recursive Programs

Authors: Martin Avanzini, Georg Moser, Michael Schaper

Abstract: In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[.], translating a pre-expectation semantic… ▽ More In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[.], translating a pre-expectation semantics into first-order constraints, susceptible to automation via standard methods. A crucial step is the use of logical variables, inspired by previous work on Hoare logics for recursive programs. Noteworthy, our methodology is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights. We have implemented this analysis in our prototype ev-imp. We provide ample experimental evidence of the prototype's algorithmic expressibility. △ Less

Submitted 24 April, 2023; v1 submitted 3 April, 2023; originally announced April 2023.

Comments: Accepted at PLDI'23

Quantum Expectation Transformers for Cost Analysis

Authors: Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, Vladimir Zamdzhiev

Abstract: We introduce a new kind of expectation transformer for a mixed classical-quantum programming language. Our semantic approach relies on a new notion of a cost structure, which we introduce and which can be seen as a specialisation of the Kegelspitzen of Keimel and Plotkin. We show that our weakest precondition analysis is both sound and adequate with respect to the operational semantics of the lang… ▽ More We introduce a new kind of expectation transformer for a mixed classical-quantum programming language. Our semantic approach relies on a new notion of a cost structure, which we introduce and which can be seen as a specialisation of the Kegelspitzen of Keimel and Plotkin. We show that our weakest precondition analysis is both sound and adequate with respect to the operational semantics of the language. Using the induced expectation transformer, we provide formal analysis methods for the expected cost analysis and expected value analysis of classical-quantum programs. We illustrate the usefulness of our techniques by computing the expected cost of several well-known quantum algorithms and protocols, such as coin tossing, repeat until success, entangled state preparation, and quantum walks. △ Less

Submitted 23 January, 2022; originally announced January 2022.

Modular Runtime Complexity Analysis of Probabilistic While Programs

Authors: Martin Avanzini, Michael Schaper, Georg Moser

Abstract: We are concerned with the average case runtime complexity analysis of a prototypical imperative language endowed with primitives for sampling and probabilistic choice. Taking inspiration from known approaches from to the modular resource analysis of non-probabilistic programs, we investigate how a modular runtime analysis is obtained for probabilistic programs. We are concerned with the average case runtime complexity analysis of a prototypical imperative language endowed with primitives for sampling and probabilistic choice. Taking inspiration from known approaches from to the modular resource analysis of non-probabilistic programs, we investigate how a modular runtime analysis is obtained for probabilistic programs. △ Less

Submitted 23 August, 2019; originally announced August 2019.

On Probabilistic Term Rewriting

Authors: Martin Avanzini, Ugo Dal Lago, Akihisa Yamada

Abstract: We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite systems are considered. Two instances of the interpretation method - polynomial and matrix interpretations - are analyzed and shown to capture interesting and… ▽ More We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite systems are considered. Two instances of the interpretation method - polynomial and matrix interpretations - are analyzed and shown to capture interesting and nontrivial examples when automated. We capture probabilistic computation in a novel way by way of multidistribution reduction sequences, this way accounting for both the nondeterminism in the choice of the redex and the probabilism intrinsic in firing each rule. △ Less

Submitted 27 February, 2018; originally announced February 2018.

Comments: Technical Report of our FLOPS'18 paper

Automating Sized Type Inference for Complexity Analysis (Technical Report)

Authors: Martin Avanzini, Ugo Dal Lago

Abstract: This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation, and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which ca… ▽ More This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation, and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to the choice of adopting an abstract index language and index polymorphism at higher ranks. A prototype implementation is available. △ Less

Submitted 28 June, 2017; originally announced June 2017.

Comments: Technical report of http://dx.doi.org/10.1145/3110287

GUBS Upper Bound Solver (Extended Abstract)

Authors: Martin Avanzini, Michael Schaper

Abstract: In this extended abstract we present the GUBS Upper Bound Solver. GUBS is a dedicated constraint solver over the naturals for inequalities formed over uninterpreted function symbols and standard arithmetic operations. GUBS now forms the backbone of HoSA, a tool for analysing space and time complexity of higher-order functional programs automatically. We give insights about the implemen- tation and… ▽ More In this extended abstract we present the GUBS Upper Bound Solver. GUBS is a dedicated constraint solver over the naturals for inequalities formed over uninterpreted function symbols and standard arithmetic operations. GUBS now forms the backbone of HoSA, a tool for analysing space and time complexity of higher-order functional programs automatically. We give insights about the implemen- tation and report different case studies. △ Less

Submitted 18 April, 2017; originally announced April 2017.

Comments: In Proceedings DICE-FOPARA 2017, arXiv:1704.05169

ACM Class: D.2.4; F.4.0

Journal ref: EPTCS 248, 2017, pp. 17-23

Automated Sized-Type Inference and Complexity Analysis

Authors: Martin Avanzini, Ugo Dal Lago

Abstract: This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of… ▽ More This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available. △ Less

Submitted 18 April, 2017; originally announced April 2017.

Comments: In Proceedings DICE-FOPARA 2017, arXiv:1704.05169

ACM Class: I.2.2

Journal ref: EPTCS 248, 2017, pp. 7-16

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version)

Authors: Martin Avanzini, Ugo Dal Lago, Georg Moser

Abstract: We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the c… ▽ More We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Further, we describe suitable strategies for the application of the studied transformations and provide ample experimental data for assessing the viability of our method. △ Less

Submitted 16 June, 2015; originally announced June 2015.

Comments: Long version of paper presented at ICFP 2015

ACM Class: F.3.2

On Sharing, Memoization, and Polynomial Time (Long Version)

Authors: Martin Avanzini, Ugo Dal Lago

Abstract: We study how the adoption of an evaluation mechanism with sharing and memoization impacts the class of functions which can be computed in polynomial time. We first show how a natural cost model in which lookup for an already computed value has no cost is indeed invariant. As a corollary, we then prove that the most general notion of ramified recurrence is sound for polynomial time, this way settli… ▽ More We study how the adoption of an evaluation mechanism with sharing and memoization impacts the class of functions which can be computed in polynomial time. We first show how a natural cost model in which lookup for an already computed value has no cost is indeed invariant. As a corollary, we then prove that the most general notion of ramified recurrence is sound for polynomial time, this way settling an open problem in implicit computational complexity. △ Less

Submitted 5 January, 2015; originally announced January 2015.

ACM Class: F.1.3; F.3.2; F.4.1; F.4.2

A New Term Rewriting Characterisation of ETIME functions

Authors: Martin Avanzini, Naohi Eguchi

Abstract: Adopting former term rewriting characterisations of polytime and exponential-time computable functions, we introduce a new reduction order, the Path Order for ETIME (POE* for short), that is sound and complete for ETIME computable functions. The proposed reduction order for ETIME makes contrasts to those related complexity classes clear. Adopting former term rewriting characterisations of polytime and exponential-time computable functions, we introduce a new reduction order, the Path Order for ETIME (POE* for short), that is sound and complete for ETIME computable functions. The proposed reduction order for ETIME makes contrasts to those related complexity classes clear. △ Less

Submitted 30 December, 2013; v1 submitted 27 December, 2013; originally announced December 2013.

Comments: Technical report

Polynomial Path Orders

Authors: Martin Avanzini, Georg Moser

Abstract: This paper is concerned with the complexity analysis of constructor term rewrite systems and its ramification in implicit computational complexity. We introduce a path order with multiset status, the polynomial path order POP*, that is applicable in two related, but distinct contexts. On the one hand POP* induces polynomial innermost runtime complexity and hence may serve as a syntactic, and full… ▽ More This paper is concerned with the complexity analysis of constructor term rewrite systems and its ramification in implicit computational complexity. We introduce a path order with multiset status, the polynomial path order POP*, that is applicable in two related, but distinct contexts. On the one hand POP* induces polynomial innermost runtime complexity and hence may serve as a syntactic, and fully automatable, method to analyse the innermost runtime complexity of term rewrite systems. On the other hand POP* provides an order-theoretic characterisation of the polytime computable functions: the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP*. △ Less

Submitted 30 October, 2013; v1 submitted 10 September, 2013; originally announced September 2013.

Comments: LMCS version. This article supersedes arXiv:1209.3793

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 4 (November 1, 2013) lmcs:807

A Haskell Library for Term Rewriting

Authors: Bertram Felgenhauer, Martin Avanzini, Christian Sternagel

Abstract: We present a Haskell library for first-order term rewriting covering basic operations on positions, terms, contexts, substitutions and rewrite rules. This effort is motivated by the increasing number of term rewriting tools that are written in Haskell. We present a Haskell library for first-order term rewriting covering basic operations on positions, terms, contexts, substitutions and rewrite rules. This effort is motivated by the increasing number of term rewriting tools that are written in Haskell. △ Less

Submitted 8 July, 2013; originally announced July 2013.

Comments: 1st International Workshop on Haskell And Rewriting Techniques, HART 2013, 6 pages

A Combination Framework for Complexity

Authors: Martin Avanzini, Georg Moser

Abstract: In this paper we present a combination framework for polynomial complexity analysis of term rewrite systems. The framework covers both derivational and runtime complexity analysis. We present generalisations of powerful complexity techniques, notably a generalisation of complexity pairs and (weak) dependency pairs. Finally, we also present a novel technique, called dependency graph decomposition,… ▽ More In this paper we present a combination framework for polynomial complexity analysis of term rewrite systems. The framework covers both derivational and runtime complexity analysis. We present generalisations of powerful complexity techniques, notably a generalisation of complexity pairs and (weak) dependency pairs. Finally, we also present a novel technique, called dependency graph decomposition, that in the dependency pair setting greatly increases modularity. We employ the framework in the automated complexity tool TCT. TCT implements a majority of the techniques found in the literature, witnessing that our framework is general enough to capture a very brought setting. △ Less

Submitted 5 February, 2013; originally announced February 2013.

ACM Class: F.1.3; F.3.2; F.4.1; F.4.2

Polynomial Path Orders: A Maximal Model

Authors: Martin Avanzini, Georg Moser

Abstract: This paper is concerned with the automated complexity analysis of term rewrite systems (TRSs for short) and the ramification of these in implicit computational complexity theory (ICC for short). We introduce a novel path order with multiset status, the polynomial path order POP*. Essentially relying on the principle of predicative recursion as proposed by Bellantoni and Cook, its distinct feature… ▽ More This paper is concerned with the automated complexity analysis of term rewrite systems (TRSs for short) and the ramification of these in implicit computational complexity theory (ICC for short). We introduce a novel path order with multiset status, the polynomial path order POP*. Essentially relying on the principle of predicative recursion as proposed by Bellantoni and Cook, its distinct feature is the tight control of resources on compatible TRSs: The (innermost) runtime complexity of compatible TRSs is polynomially bounded. We have implemented the technique, as underpinned by our experimental evidence our approach to the automated runtime complexity analysis is not only feasible, but compared to existing methods incredibly fast. As an application in the context of ICC we provide an order-theoretic characterisation of the polytime computable functions. To be precise, the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP*. △ Less

Submitted 17 September, 2012; originally announced September 2012.

ACM Class: F.2.2; F.4.1; F.4.2; D.2.4; D.2.8

A New Order-theoretic Characterisation of the Polytime Computable Functions

Authors: Martin Avanzini, Naohi Eguchi, Georg Moser

Abstract: We propose a new order, the small polynomial path order (sPOP* for short). The order sPOP* provides a characterisation of the class of polynomial time computable function via term rewrite systems. Any polynomial time computable function gives rise to a rewrite system that is compatible with sPOP*. On the other hand any function defined by a rewrite system compatible with sPOP* is polynomial time c… ▽ More We propose a new order, the small polynomial path order (sPOP* for short). The order sPOP* provides a characterisation of the class of polynomial time computable function via term rewrite systems. Any polynomial time computable function gives rise to a rewrite system that is compatible with sPOP*. On the other hand any function defined by a rewrite system compatible with sPOP* is polynomial time computable. Technically sPOP* is a tamed recursive path order with product status. Its distinctive feature is the precise control provided. For any rewrite system that is compatible with sPOP* that makes use of recursion up to depth d, the (innermost) runtime complexity is bounded from above by a polynomial of degree d. △ Less

Submitted 16 January, 2012; v1 submitted 12 January, 2012; originally announced January 2012.

Comments: Technical Report

ACM Class: F.2.2; F.4.1; F.4.2; D.2.4; D.2.8

A Path Order for Rewrite Systems that Compute Exponential Time Functions (Technical Report)

Authors: Martin Avanzini, Naohi Eguchi, Georg Moser

Abstract: In this paper we present a new path order for rewrite systems, the exponential path order EPOSTAR. Suppose a term rewrite system is compatible with EPOSTAR, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPOSTAR equals the class of functions computable in exponentia… ▽ More In this paper we present a new path order for rewrite systems, the exponential path order EPOSTAR. Suppose a term rewrite system is compatible with EPOSTAR, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPOSTAR equals the class of functions computable in exponential time on a Turing maschine. △ Less

Submitted 9 June, 2011; v1 submitted 6 October, 2010; originally announced October 2010.

Comments: Technical Report

MSC Class: 03D15

Efficient Implementation of Rewriting Revisited Technical Report

Authors: Martin Avanzini, Georg Moser

Abstract: Recently, many techniques have been introduced that allow the (automated) classification of the runtime complexity of term rewrite systems (TRSs for short). In earlier work, the authors have shown that for confluent TRSs, innermost polynomial runtime complexity induces polytime computability of the functions defined. In this paper, we generalise the above result to full rewriting. Following our… ▽ More Recently, many techniques have been introduced that allow the (automated) classification of the runtime complexity of term rewrite systems (TRSs for short). In earlier work, the authors have shown that for confluent TRSs, innermost polynomial runtime complexity induces polytime computability of the functions defined. In this paper, we generalise the above result to full rewriting. Following our previous work, we exploit graph rewriting. We give a new proof of the adequacy of graph rewriting for full rewriting that allows for a precise control of the resources copied. In sum we completely describe an implementation of rewriting on a Turing machine (TM for short). We show that the runtime complexity of the TRS and the runtime complexity of the TM is polynomially related. Our result strengthens the evidence that the complexity of a rewrite system is truthfully represented through the length of derivations. Moreover our result allows the classification of non-deterministic polytime-computation based on runtime complexity analysis of rewrite systems. △ Less

Submitted 8 June, 2011; v1 submitted 29 January, 2010; originally announced January 2010.

Comments: Submitted to RTA 2010

ACM Class: F.1.2; F.1.3; F.4.2

Dependency Pairs and Polynomial Path Orders

Authors: Martin Avanzini, Georg Moser

Abstract: We show how polynomial path orders can be employed efficiently in conjunction with weak innermost dependency pairs to automatically certify polynomial runtime complexity of term rewrite systems and the polytime computability of the functions computed. The established techniques have been implemented and we provide ample experimental data to assess the new method. We show how polynomial path orders can be employed efficiently in conjunction with weak innermost dependency pairs to automatically certify polynomial runtime complexity of term rewrite systems and the polytime computability of the functions computed. The established techniques have been implemented and we provide ample experimental data to assess the new method. △ Less

Submitted 8 June, 2011; v1 submitted 6 April, 2009; originally announced April 2009.

Comments: 23 pages, conference version accepted at RTA 2009