FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
VolCE: An Efficient Tool for Solving #SMT(LA) Problems

Authors: Cunjing Ge, Feifei Ma and Jian Zhang

Paper Information

Title:VolCE: An Efficient Tool for Solving #SMT(LA) Problems
Authors:Cunjing Ge, Feifei Ma and Jian Zhang
Proceedings:PRUV PRUV 2018 Proceedings
Editors: Thomas Lukasiewicz, Rafael PeƱaloza and Anni-Yasmin Turhan
Keywords:Model Counting, Volume Computation, Volume Estimation, #SMT(LA)
Abstract:

ABSTRACT. We present VolCE, a tool for computing and estimating the size of the solution space of SMT(LA) constraints. VolCE supports the SMT-LIB format. It integrates SMT solving with volume computation/estimation and integer solution counting for convex polytopes. Several effective techniques are adopted, which enable the tool to deal with high-dimensional problem instances efficiently.

Pages:8
Talk:Jul 19 17:30 (Session 136D: PRUV regular papers)
Paper: