- -

SAT modulo linear arithmetic for Solving Polynomial Constraints

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

SAT modulo linear arithmetic for Solving Polynomial Constraints

Show simple item record

Files in this item

dc.contributor.author Borralleras, Cristina es_ES
dc.contributor.author Lucas Alba, Salvador es_ES
dc.contributor.author Oliveras ., Albert es_ES
dc.contributor.author Rodriguez-Carbonell, Enric es_ES
dc.contributor.author Rubio ., Albert es_ES
dc.date.accessioned 2014-05-21T16:13:48Z
dc.date.issued 2012-01
dc.identifier.issn 0168-7433
dc.identifier.uri http://hdl.handle.net/10251/37666
dc.description.abstract 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. es_ES
dc.description.sponsorship 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. en_EN
dc.format.extent 25 es_ES
dc.language Inglés es_ES
dc.publisher Springer Netherlands es_ES
dc.relation EU es_ES
dc.relation Spanish MEC/MICINN [TIN 2007-68093-C02-01, TIN 2007-68093-C02-02] es_ES
dc.relation.ispartof Journal of Automated Reasoning es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Constraint solving es_ES
dc.subject Non-linear arithmetic es_ES
dc.subject Polynomial constraints es_ES
dc.subject SAT modulo theories es_ES
dc.subject System verification es_ES
dc.subject Termination es_ES
dc.subject Hardware and software es_ES
dc.subject Linear arithmetic es_ES
dc.subject Non-linear constraints es_ES
dc.subject Program invariants es_ES
dc.subject Satisfiability es_ES
dc.subject System verifications es_ES
dc.subject Unsatisfiable core es_ES
dc.subject Formal logic es_ES
dc.subject Hybrid systems es_ES
dc.subject Polynomials es_ES
dc.subject Verification es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title SAT modulo linear arithmetic for Solving Polynomial Constraints es_ES
dc.type Artículo es_ES
dc.embargo.lift 10000-01-01
dc.embargo.terms forever es_ES
dc.identifier.doi 10.1007/s10817-010-9196-8
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation 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 es_ES
dc.description.accrualMethod Senia es_ES
dc.relation.publisherversion http://link.springer.com/article/10.1007%2Fs10817-010-9196-8 es_ES
dc.description.upvformatpinicio 107 es_ES
dc.description.upvformatpfin 131 es_ES
dc.type.version info:eu repo/semantics/publishedVersion es_ES
dc.description.volume 48 es_ES
dc.description.issue 1 es_ES
dc.relation.senia 230141
dc.identifier.eissn 1573-0670


This item appears in the following Collection(s)

Show simple item record