- -

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 completo del ítem

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

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/37666

Ficheros en el ítem

Thumbnail
Nombre: Borralleras, Lucas, ...
Tamaño: 304.0Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir/Preview
[Cerrado]
Nombre: Lucas - SAT modulo ...
Tamaño: 470.5Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: SAT modulo linear arithmetic for Solving Polynomial Constraints
Autor: Borralleras, Cristina Lucas Alba, Salvador Oliveras ., Albert Rodriguez-Carbonell, Enric Rubio ., Albert
Entidad UPV: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Fecha difusión:
Resumen:
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 ...[+]
Palabras clave: Constraint solving , Non-linear arithmetic , Polynomial constraints , SAT modulo theories , System verification , Termination , Hardware and software , Linear arithmetic , Non-linear constraints , Program invariants , Satisfiability , System verifications , Unsatisfiable core , Formal logic , Hybrid systems , Polynomials , Verification
Derechos de uso: Reserva de todos los derechos
Fuente:
Journal of Automated Reasoning. (issn: 0168-7433 ) (eissn: 1573-0670 )
DOI: 10.1007/s10817-010-9196-8
Editorial:
Springer Netherlands
Versión del editor: http://link.springer.com/article/10.1007%2Fs10817-010-9196-8
Código del Proyecto:
info:eu-repo/grantAgreement/MEC//TIN2007-68093-C02-02/ES/TECHNOLOGICS-UPV/
info:eu-repo/grantAgreement/MEC//TIN2007-68093-C02-01/ES/LOGICTOOLS-2/
Agradecimientos:
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.
Tipo: Artículo

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)

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) [+]
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, 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)

Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. Springer (2003)

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)

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)

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)

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)

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)

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)

de Moura, L., Olney Passmore, G.: On Locally Minimal Nullstellensatz Proofs. Technical Report, Microsoft Research, MSR-TR-2009-90.pdf (2009)

Doltzmann, A., Sturm, T.: REDLOG: Computer Algebra Meets Computer Logic. Technical Report, University of Passau, MIP-9603 (1996)

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)

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)

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)

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)

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)

Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco (1979)

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)

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)

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)

Hofbauer, D., Waldmann, J.: Termination of {aa → bc, bb → ac, cc → ab}. Inf. Process. Lett. 98(4), 156–158 (2006)

Hong, H., et al.: http://www.usna.edu/Users/cs/qepcad/B/WhatisQEPCAD.html . Accessed June 2010

Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proceedings of the IMACS International Conference on Applications of Computer Algebra (2004)

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)

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

Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO ITA 39(3), 547–586 (2005)

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)

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)

Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)

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)

Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods in Syst. Des. 32(1), 25–55 (2008)

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)

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)

Stengle, G.: A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann. 207(2), 87–97 (1973)

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)

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)

[-]

recommendations

 

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

Mostrar el registro completo del ítem