- -

SAT modulo linear arithmetic for Solving Polynomial Constraints

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

SAT modulo linear arithmetic for Solving Polynomial Constraints

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: Borralleras, Lucas, ...
Tamaño: 304.0Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Lucas - SAT modulo ...
Tamaño: 470.5Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
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.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.relation.projectID info:eu-repo/grantAgreement/MEC//TIN2007-68093-C02-02/ES/TECHNOLOGICS-UPV/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MEC//TIN2007-68093-C02-01/ES/LOGICTOOLS-2/ es_ES
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. https://doi.org/10.1007/s10817-010-9196-8 es_ES
dc.description.accrualMethod S 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
dc.contributor.funder Ministerio de Educación y Ciencia es_ES
dc.description.references 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) es_ES
dc.description.references Barrett, C., Deters, M., Oliveras, A., Stump, A.: The Satisfiability Modulo Theories Competition (SMT-COMP). http://www.smtcomp.org (2009) es_ES
dc.description.references Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). http://www.smt-lib.org (2008) es_ES
dc.description.references Barrett, C., Tinelli, C.: CVC3. In: Proceedings of the 19th International Conference on Computer Aided Verification, CAV’07. Lecture Notes in Computer Science, vol. 4590, pp. 298–302. Springer (2007) es_ES
dc.description.references Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. Springer (2003) es_ES
dc.description.references Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The Barcelogic SMT solver. In: Proceedings of the 20th International Conference on Computer Aided Verification, CAV’08. Lecture Notes in Computer Science, vol. 5123, pp. 294–298. Springer (2008) es_ES
dc.description.references Borralleras, C., Lucas, S., Navarro-Marset, R., Rodríguez-Carbonell, E., Rubio, A.: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In: Proceedings of the 22nd International Conference on Automated Deduction, CADE-22. Lecture Notes in Computer Science, vol. 5663, pp. 294–305. Springer (2009) es_ES
dc.description.references Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Proceedings of 15th International Conference on Computer Aided Verification, CAV’03. Lecture Notes in Computer Science, vol. 2725, pp. 420–432. Springer (2003) es_ES
dc.description.references Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J Autom Reason 34(4), 325–363. Springer (2006) es_ES
dc.description.references Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL’78, pp. 84–96. ACM Press (1978) es_ES
dc.description.references de Moura, L., Björner, N.: Z3: An efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008) es_ES
dc.description.references de Moura, L., Olney Passmore, G.: On Locally Minimal Nullstellensatz Proofs. Technical Report, Microsoft Research, MSR-TR-2009-90.pdf (2009) es_ES
dc.description.references Doltzmann, A., Sturm, T.: REDLOG: Computer Algebra Meets Computer Logic. Technical Report, University of Passau, MIP-9603 (1996) es_ES
dc.description.references Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of the 18th International Conference on Computer Aided Verification, CAV’06. Lecture Notes in Computer Science, vol. 4144, pp. 81–94. Springer (2006) es_ES
dc.description.references Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1(3–4), 209–236 (2007) es_ES
dc.description.references Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT’07. Lecture Notes in Computer Science, vol. 4501, pp. 340–354. Springer (2007) es_ES
dc.description.references Fuhs, C., Navarro-Marset, R., Otto, C., Giesl, J., Lucas, S., Schneider-Kamp, P.: Search techniques for rational polynomial orders. In: Proceedings of the 9th International Conference on Intelligent Computer Mathematics, AISC’08. Lecture Notes in Computer Science, vol. 5144, pp. 109–124. Springer (2008) es_ES
dc.description.references Ganai, M.K., Ivanc̆ić, F.: Efficient decision procedure for non-linear arithmetic constraints using CORDIC. In: Proceedings of the 9th International Conference on Formal Methods in Computer Aided Design, FMCAD’09, pp. 61–68. IEEE (2009) es_ES
dc.description.references Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco (1979) es_ES
dc.description.references Giesl, J.: Generating polynomial orderings for termination proofs. In: Proceedings of the 6th International Conference on Rewriting Techniques and Applications, RTA’95. Lecture Notes in Computer Science, vol. 914, pp. 426–431. Springer (1995) es_ES
dc.description.references Giesl, J., Schneider-Kamp, P., Thiemann, R.: Automatic termination proofs in the dependency pair framework. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning, IJCAR’06. Lecture Notes in Computer Science, vol. 4130, pp. 281–286. Springer (2006) es_ES
dc.description.references Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, PLDI’08, pp. 281–292. ACM Press, New York (2008) es_ES
dc.description.references Hofbauer, D., Waldmann, J.: Termination of {aa → bc, bb → ac, cc → ab}. Inf. Process. Lett. 98(4), 156–158 (2006) es_ES
dc.description.references Hong, H., et al.: http://www.usna.edu/Users/cs/qepcad/B/WhatisQEPCAD.html . Accessed June 2010 es_ES
dc.description.references Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proceedings of the IMACS International Conference on Applications of Computer Algebra (2004) es_ES
dc.description.references Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Proceedings of the 2nd International Workshop on Hybrid Systems: Computation and Control, HSCC’99. Lecture Notes in Computer Science, vol. 1569, pp. 137–151. Springer (1999) es_ES
dc.description.references Lucas, S.: MU-TERM: a tool for proving termination of context-sensitive rewriting. In: Proceedings of the 15th International Conference on Rewriting Techniques and Applications, RTA’04. Lecture Notes in Computer Science, vol. 3091, pp. 200–209. Springer (2004). http://zenon.dsic.upv.es/muterm . Accessed June 2010 es_ES
dc.description.references Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO ITA 39(3), 547–586 (2005) es_ES
dc.description.references Lucas, S.: Practical use of polynomials over the reals in proofs of termination. In: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’07, pp. 39–50. ACM Press, New York (2007) es_ES
dc.description.references Nguyen, M.T., De Schreye, D.: Polynomial interpretations as a basis for termination analysis of logic programs. In: Proceedings of the 21st International Conference on Logic Programming, ICLP’05. Lecture Notes in Computer Science, vol. 3668, pp. 311–325. Springer (2005) es_ES
dc.description.references Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003) es_ES
dc.description.references Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Proceedings of the 11th International Symposium on Static Analysis, SAS’04. Lecture Notes in Computer Science, vol. 3148, pp. 53–68 (2004) es_ES
dc.description.references Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods in Syst. Des. 32(1), 25–55 (2008) es_ES
dc.description.references Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: Proceedings of the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL’04, pp. 318–329. ACM Press, New York (2004) es_ES
dc.description.references Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, ASE’03, pp. 94–105. IEEE Computer Society (2003) es_ES
dc.description.references Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87–97 (1973) es_ES
dc.description.references Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Proceedings of the 19th International Workshop on Computer Science Logic, CSL’05. Lecture Notes in Computer Science, vol. 3634, pp. 248–262 (2005) es_ES
dc.description.references Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-16 (2010) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem