OptiMathSAT

To appear.

@inproceedings{cade_st19,
  author    = {Patrick Trentin and
               Roberto Sebastiani},
  title     = {Optimization Modulo the Theory of Floating-Point Numbers},
  booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on
               Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
  pages     = {550--567},
  year      = {2019},
  crossref  = {DBLP:conf/cade/2019},
  url       = {https://doi.org/10.1007/978-3-030-29436-6\_33},
  doi       = {10.1007/978-3-030-29436-6\_33},
  timestamp = {Wed, 21 Aug 2019 13:45:44 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/TrentinS19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{st_jar18,
    author  = "Sebastiani, Roberto and Trentin, Patrick",
    title   = "OptiMathSAT: A Tool for Optimization Modulo Theories",
    journal = "Journal of Automated Reasoning",
    year    = "2018",
    month   = "Dec",
    day     = "15",
    issn    = "1573-0670",
    doi     = "10.1007/s10817-018-09508-6",
    url     = "https://doi.org/10.1007/s10817-018-09508-6"
}

@InProceedings{st_tacas17,
    author       = {Roberto Sebastiani and Patrick Trentin},
    title        = {On Optimization Modulo Theories, MaxSMT and Sorting Networks},
    optcrossref  = {},
    optkey       = {},
    booktitle    = {Proc. Int. Conference on Tools and Algorithms for the
                   Construction and Analysis of Systems, TACAS'17},
    year         = {2017},
    opteditor    = {},
    volume       = {10205},
    optnumber    = {},
    series       = {LNCS},
    optpages     = {},
    optmonth     = {},
    optaddress   = {},
    optorganization = {},
    publisher    = {Springer},
    optnote      = {},
    optannote    = {}
}

@InProceedings{st_cav15,
    author       = {Roberto Sebastiani and Patrick Trentin},
    title        = {{OptiMathSAT: A Tool for Optimization Modulo Theories.}},
    booktitle    = {Proc. International Conference on Computer-Aided
                   Verification, CAV 2015},
    optbooktitle = {Proc. CAV},
    optpages     = {},
    year         = {2015},
    opteditor	 = {},
    volume       = {9206},
    optnumber	 = {},
    series       = {LNCS},
    optaddress	 = {},
    optmonth	 = {},
    optorganization = {},
    publisher	 = {Springer},
    optnote      = {},
    optannote	 = {}
}

@InProceedings{st_tacas15,
    author       = {Roberto Sebastiani and Patrick Trentin},
    title        = {{Pushing the Envelope of Optimization Modulo Theories with
                   Linear-Arithmetic Cost Functions}},
    booktitle    = {Proc. Int. Conference on Tools and Algorithms for the
                   Construction and Analysis of Systems, TACAS'15},
    optbooktitle = {Proc. TACAS},
    optpages     = {},
    year         = {2015},
    opteditor    = {},
    volume       = {9035},
    optnumber    = {},
    series       = {LNCS},
    optaddress   = {},
    optmonth     = {},
    optorganization = {},
    publisher    = {Springer},
    optnote      = {},
    optannote    = {}
}

@Article{st_tocl14,
    author       = {Roberto Sebastiani and Silvia Tomasi},
    title        = {{Optimization Modulo Theories with Linear Rational
                   Costs}},
    journal      = {ACM Transactions on Computational Logics},
    year         = {2015},
    optkey       = {},
    volume       = {16},
    number       = {2},
    optpages     = {},
    month        = {March},
    optnote      = {},
    annote       = {Available at \url{http://http://tocl.acm.org/}.}
}

@InProceedings{st-ijcar12,
    author       = {Roberto Sebastiani and Silvia Tomasi},
    title        = {{Optimization in SMT with LA(Q) Cost Functions}},
    year         = {2012},
    month        = {July},
    series       = {LNAI},
    publisher    = {Springer},
    volume       = {7364},
    booktitle    = {IJCAR},
    pages        = {484-498},
    ee           = {http://dx.doi.org/10.1007/978-3-642-31365-3_38},
    optcrossref  = {dblp:conf/cade/2012},
    bibsource    = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{st-ijcar12-extended,
    author       = {Roberto Sebastiani and Silvia Tomasi},
    title        = {{Optimization in SMT with LA(Q) Cost Functions}},
    institution  = {DISI, University of Trento},
    year         = {2012},
    optkey       = {},
    opttype      = {},
    number       = {DISI-12-003},
    optaddress   = {},
    month        = {January},
    note         = {\mbox{\url{http://disi.unitn.it/~rseba/ijcar12/DISI-12-003.pdf}}},
    optannote    = {}
}