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 language | English |
|---|---|
| Title of host publication | Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 |
| Publisher | Springer |
| Publication date | 2015 |
| Pages | 194-199 |
| ISBN (Print) | 978-3-662-46680-3 |
| ISBN (Electronic) | 978-3-662-46681-0 |
| DOIs | |
| Publication status | Published - 2015 |
| Event | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015) - London, United Kingdom Duration: 11 Apr 2015 → 18 Apr 2015 Conference number: 21 http://www.etaps.org/index.php/2015/tacas |
Conference
| Conference | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015) |
|---|---|
| Number | 21 |
| Country/Territory | United Kingdom |
| City | London |
| Period | 11/04/2015 → 18/04/2015 |
| Other | Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 |
| Internet address |
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 9035 |
| ISSN | 0302-9743 |