vZ - An Optimizing SMT Solver

Nikolaj Bjørner, Phan Anh Dung, Lars Fleckenstein

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

856 Downloads (Pure)

Abstract

vZ is a part of the SMT solver Z3. It allows users to pose and solve optimization problems modulo theories. Many SMT applications use models to provide satisfying assignments, and a growing number of these build on top of Z3 to get optimal assignments with respect to objective functions. vZ provides a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. Objective functions are combined as either Pareto fronts, lexicographically, or each objective is optimized independently. We describe usage scenarios of vZ, outline the tool architecture that allows dispatching problems to special purpose solvers, and examine use cases.
Original languageEnglish
Title of host publicationProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015
PublisherSpringer
Publication date2015
Pages194-199
ISBN (Print)978-3-662-46680-3
ISBN (Electronic)978-3-662-46681-0
DOIs
Publication statusPublished - 2015
Event21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015) - London, United Kingdom
Duration: 11 Apr 201518 Apr 2015
Conference number: 21
http://www.etaps.org/index.php/2015/tacas

Conference

Conference21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)
Number21
CountryUnited Kingdom
CityLondon
Period11/04/201518/04/2015
OtherHeld as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Internet address
SeriesLecture Notes in Computer Science
Volume9035
ISSN0302-9743

Fingerprint Dive into the research topics of 'vZ - An Optimizing SMT Solver'. Together they form a unique fingerprint.

Cite this