Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/10854/1887

SAT Modulo Linear Arithmetic for Solving Polynomial
Borralleras Andreu, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert
Universitat de Vic. Escola Politècnica Superior; Universitat de Vic. Grup de Recerca en Tecnologies Digitals
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.
-Aritmètica
(c) Springer (The original publication is available at www.springerlink.com)
Tots els drets reservats
Artículo
Artículo - Versión aceptada
         

Documentos con el texto completo de este documento

Ficheros Tamaño Formato Vista
artconlli_a2012 ... as_cristina_sat_modulo.pdf 275.4 KB application/pdf Vista/Abrir

Mostrar el registro completo del ítem

Documentos relacionados

Otros documentos del mismo autor/a