E-resources
-
Trentin, Patrick; Sebastiani, Roberto
Journal of automated reasoning, 10/2021, Volume: 65, Issue: 7Journal Article
Optimization modulo theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or Pseudo-Boolean terms. However, many SMT and OMT applications, in particular from SW and HW verification, require handling bit-precise representations of numbers, which in SMT are handled by means of the theory of bit-vectors ( B V ) for the integers and that of floating-point numbers ( FP ) for the reals respectively. Whereas an approach for OMT with (unsigned) B V objectives has been proposed by Nadel & Ryvchin, unfortunately we are not aware of any existing approach for OMT with FP objectives. In this paper we fill this gap, and we address for the first time OMT with FP objectives. We present a novel OMT approach, based on the novel concept of attractor and dynamic attractor , which extends the work of Nadel and Ryvchin to work with signed- B V objectives and, most importantly, with FP objectives. We have implemented some novel OMT procedures on top of OptiMathSAT and tested them on modified problems from the SMT-LIB repository. The empirical results support the validity and feasibility of our novel approach.
Shelf entry
Permalink
- URL:
Impact factor
Access to the JCR database is permitted only to users from Slovenia. Your current IP address is not on the list of IP addresses with access permission, and authentication with the relevant AAI accout is required.
Year | Impact factor | Edition | Category | Classification | ||||
---|---|---|---|---|---|---|---|---|
JCR | SNIP | JCR | SNIP | JCR | SNIP | JCR | SNIP |
Select the library membership card:
If the library membership card is not in the list,
add a new one.
DRS, in which the journal is indexed
Database name | Field | Year |
---|
Links to authors' personal bibliographies | Links to information on researchers in the SICRIS system |
---|
Source: Personal bibliographies
and: SICRIS
The material is available in full text. If you wish to order the material anyway, click the Continue button.