VMTL: a modular termination laboratory. The automated analysis of termination of term rewriting systems (TRSs) has drawn a lot of attention in the scientific community during the last decades and many different methods and approaches have been developed for this purpose. We present VMTL (Vienna Modular Termination Laboratory), a tool implementing some of the most recent and powerful algorithms for termination analysis of TRSs, while providing an open interface that allows users to easily plug in new algorithms in a modular fashion according to the widely adopted dependency pair framework. Apart from modular extensibility, VMTL focuses on analyzing the termination behaviour of conditional term rewriting systems (CTRSs). Using one of the latest transformational techniques, the resulting restricted termination problems (for unconditional context-sensitive TRSs) are processed with dedicated algorithms.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Nishida, Naoki; Vidal, German: Program inversion for tail recursive functions (2011)
- Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador: Context-sensitive dependency pairs (2010)
- Gutiérrez, Raúl; Lucas, Salvador: Proving termination in the context-sensitive dependency pair framework (2010)
- Schernhammer, Felix; Gramlich, Bernhard: Characterizing and proving operational termination of deterministic conditional term rewriting systems (2010)