Mathias Preiner, Aina Niemetz, Armin Biere,
"Counterexample-Guided Model Synthesis"
: Proc. 23rd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17)/ Lecture Notes in Computer Science (LNCS), Serie Lecture Notes in Computer Science (LNCS), Vol. 10205, Springer, Seite(n) 264-280, 5-2017
Original Titel:
Counterexample-Guided Model Synthesis
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 23rd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17)/ Lecture Notes in Computer Science (LNCS)
Original Kurzfassung:
In this paper we present a new approach for solving quanti?ed formulas in Satis?ability Modulo Theories (SMT), with a particular focus on the theory of ?xed-size bit-vectors. We combine counterexampleguided quanti?er instantiation with a syntax-guided synthesis approach, which allows us to synthesize both Skolem functions and terms for quanti?er instantiations. Our approach employs two ground theory solvers to reason about quanti?ed formulas. It neither relies on quanti?er speci?c simpli?cations nor heuristic quanti?er instantiation techniques, which makes it a simple yet e?ective approach for solving quanti?ed formulas. We implemented our approach in our SMT solver Boolector and show in our experiments that our techniques are competitive compared to the state-of-the-art in solving quanti?ed bit-vectors.
Forschungs-