Name
Abstract | ||
|---|---|---|
Polynomial constraint-solving plays a prominent role in several areas of engineering and software verification. In particular, polynomial constraint solving has a long and successful history in the development of tools for proving termination of programs. Well-known and very efficient techniques, like SAT algorithms and tools, have been recently proposed and used for implementing polynomial constraint solving algorithms through appropriate encodings. However, powerful techniques like the ones provided by the SMT (SAT modulo theories) approach for linear arithmetic constraints (over the rationals) are underexplored to date. In this paper we show that the use of these techniques for developing polynomial constraint solvers outperforms the best existing solvers and provides a new and powerful approach for implementing better and more general solvers for termination provers. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02959-2_23 | CADE |
Keywords | Field | DocType |
sat algorithm,existing solvers,non-linear polynomial arithmetic,powerful approach,linear arithmetic constraint,polynomial constraint solvers,powerful technique,general solvers,polynomial constraint,sat modulo linear arithmetic,sat modulo theory,polynomial constraint-solving,program analysis,termination | Discrete mathematics,Rational number,Polynomial arithmetic,Nonlinear system,Polynomial,Modulo,Computer science,Algorithm,Program analysis,Linear arithmetic,Software verification | Conference |
Volume | ISSN | Citations |
5663 | 0302-9743 | 21 |
PageRank | References | Authors |
1.05 | 17 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cristina Borralleras | 1 | 126 | 7.68 |
| Salvador Lucas | 2 | 134 | 6.19 |
| Rafael Navarro-Marset | 3 | 49 | 2.70 |
| Enric Rodríguez-Carbonell | 4 | 446 | 26.13 |
| Albert Rubio | 5 | 228 | 19.44 |