Loading...
Please wait, while we are loading the content...
Similar Documents
2 4 6 8 10 12 14 2 3 5 7 9 13 15 20 25 30 35 40 45
| Content Provider | Semantic Scholar |
|---|---|
| Author | Milicevic, Aleksandar Near, Joseph P. Kang, Eunsuk Jackson, Daniel |
| Copyright Year | 2014 |
| Abstract | The last decade has seen a dramatic growth in the use of constraint solvers as a computational mechanism, not only for analysis and synthesis of software, but also at runtime. Solvers are available for a variety of logics but are generally restricted to first-order formulas. Some tasks, however, most notably those involving synthesis, are inherently higher order; these are typically handled by embedding a first-order solver (such as a SAT or SMT solver) in a domain-specific algorithm. Using strategies similar to those used in such algorithms, we show how to extend a first-order solver (in this case Kodkod, a model finder for relational logic used as the engine of the Alloy Analyzer) so that it can handle quantifications over higher-order structures. The resulting solver is sufficiently general that it can be applied to a range of problems; it is higher order, so that it can be applied directly, without embedding in another algorithm; and it performs well enough to be competitive with specialized tools on standard benchmarks. Although the approach is demonstrated for a particular relational logic, the principles behind it could be applied to other first-order solvers. Just as the identification of first-order solvers as reusable backends advanced the performance of specialized tools and simplified their architecture, factoring out higher-order solvers may bring similar benefits to a new class of tools. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://dspace.mit.edu/openaccess-disseminate/1721.1/116144 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
