2014/10/21 by Roberto Sebastiani, Sebastiani, Roberto, Patrick Trentin +1
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Safety Systems Engineering in Autonomy
paper · pdf · doi:10.48550/arxiv.1410.5568
openalex publication_date 2014/10/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In the last decade we have witnessed an impressive progress in the\nexpressiveness and efficiency of Satisfiability Modulo Theories (SMT) solving\ntechniques. This has brought previously-intractable problems at the reach of\nstate-of-the-art SMT solvers, in particular in the domain of SW and HW\nverification. Many SMT-encodable problems of interest, however, require also\nthe capability of finding models that are optimal wrt. some cost functions. In\nprevious work, namely "Optimization Modulo Theory with Linear Rational Cost\nFunctions -- OMT(LAR U T )", we have leveraged SMT solving to handle the\nminimization of cost functions on linear arithmetic over the rationals, by\nmeans of a combination of SMT and LP minimization techniques. In this paper we\npush the envelope of our OMT approach along three directions: first, we extend\nit to work also with linear arithmetic on the mixed integer/rational domain, by\nmeans of a combination of SMT, LP and ILP minimization techniques; second, we\ndevelop a multi-objective version of OMT, so that to handle many cost functions\nsimultaneously; third, we develop an incremental version of OMT, so that to\nexploit the incrementality of some OMT-encodable problems. An empirical\nevaluation performed on OMT-encoded verification problems demonstrates the\nusefulness and efficiency of these extensions.\n