Suchergebnisse

Context-sensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions of subterms that can be rewritten; or frozen, i.e., positions that cannot. Frozen positions can be used to denote subexpressions whose evaluation is delayed or just forbidden. A typical example is the if-then-else operator whose second and third arguments are not evaluated until the evaluation of the first argument yields either true or false. Imposing replacement restrictions can improve the termination behavior of rewriting-based computational systems. Termination of CSR has been investigated by several authors and a number of automatic tools are able to prove it. In this paper, we analyze how frozen subterms affect termination of CSR. This analysis helps us to improve our context-sensitive dependency pair (CS-DP) framework for automatically proving termination of CSR. We have implemented these improvements in our tool MU-TERM. The experiments show the power of the improvements in practice. Gutiérrez Gil, R.; Lucas Alba, S. (2015). Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting. http://hdl.handle.net/10251/50750

107 131 48 1 ; S Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87–97 (1973) ; Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g.; termination proving, program invariant generation and hybrid system verification, to name a few. In this paper we propose a new method for solving non-linear constraints based on encoding the problem into an SMT problem considering only linear arithmetic. Unlike other existing methods, our method focuses on proving satisfiability of the constraints rather than on proving unsatisfiability, which is more relevant in several applications as we illustrate with several examples. Nevertheless, we also present new techniques based on the analysis of unsatisfiable cores that allow one to efficiently prove unsatisfiability too for a broad class of problems. The power of our approach is demonstrated by means of extensive experiments comparing our prototype with state-of-the-art tools on benchmarks taken both from the academic and the industrial world. © 2010 Springer Science+Business Media B.V. This work has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN, under grants TIN 2007-68093-C02-01 and TIN 2007-68093-C02-02. Borralleras, C.; Lucas Alba, S.; Oliveras ., A.; Rodriguez-Carbonell, E.; Rubio ., A. (2012). SAT modulo linear arithmetic for Solving Polynomial Constraints. Journal of Automated Reasoning. 48(1):107-131. doi:10.1007/s10817-010-9196-8 Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of the 13th International Conference on Algebraic Methodology and Software Technology, AMAST'10 (2010) Barrett, C., Deters, M., Oliveras, A., Stump, A.: The Satisfiability Modulo Theories Competition (SMT-COMP). http://www.smtcomp.org (2009) Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). http://www.smt-lib.org (2008) Barrett, ...