Counterexample-guided model synthesis. (English) Zbl 1452.68122
Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 264-280 (2017).
Summary: In this paper we present a new approach for solving quantified formulas in Satisfiability Modulo Theories (SMT), with a particular focus on the theory of fixed-size bit-vectors. We combine counterexample-guided quantifier instantiation with a syntax-guided synthesis approach, which allows us to synthesize both Skolem functions and terms for quantifier instantiations. Our approach employs two ground theory solvers to reason about quantified formulas. It neither relies on quantifier specific simplifications nor heuristic quantifier instantiation techniques, which makes it a simple yet effective approach for solving quantified 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 quantified bit-vectors.
For the entire collection see [Zbl 1360.68015].
For the entire collection see [Zbl 1360.68015].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B70 | Logic in computer science |
References:
| [1] | Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 120-135. Springer, Heidelberg (2008). doi:10.1007/978-3-540-93900-9_13 · Zbl 1206.68087 · doi:10.1007/978-3-540-93900-9_13 |
| [2] | Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 236-250. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_19 · Zbl 1284.68172 · doi:10.1007/978-3-642-12002-2_19 |
| [3] | Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17-23 January 2010, pp. 313-326. ACM (2010) · Zbl 1312.68068 |
| [4] | Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: 6th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2006, San Jose, California, USA, 12-16 November 2006, Proceedings, pp. 117-124. IEEE Computer Society (2006) |
| [5] | Kovásznai, G., Fröhlich, A., Biere, A.: Complexity of fixed-size bit-vector logics. Theory Comput. Syst. 59(2), 323-376 (2016) · Zbl 1357.68086 · doi:10.1007/s00224-015-9653-1 |
| [6] | Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171-177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14 · doi:10.1007/978-3-642-22110-1_14 |
| [7] | Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24 · doi:10.1007/978-3-540-78800-3_24 |
| [8] | Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737-744. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_49 · doi:10.1007/978-3-319-08867-9_49 |
| [9] | Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 198-216. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_12 · Zbl 1381.68059 · doi:10.1007/978-3-319-21668-3_12 |
| [10] | Ge, Y., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306-320. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_25 · Zbl 1242.68280 · doi:10.1007/978-3-642-02658-4_25 |
| [11] | Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. In: Bloem, R., Sharygina, N. (eds.) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, 20-23 October, pp. 239-246. IEEE (2010) · Zbl 1284.03212 |
| [12] | Dutertre, B.: Solving exists/forall problems in Yices. In: Workshop on Satisfiability Modulo Theories (2015) |
| [13] | Jonáš, M., Strejček, J.: Solving quantified bit-vector formulas using binary decision diagrams. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 267-283. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40970-2_17 · Zbl 1475.68345 · doi:10.1007/978-3-319-40970-2_17 |
| [14] | Alur, R., Bodík, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20-23 October 2013, pp. 1-8. IEEE (2013) |
| [15] | Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 2s. Elsevier and MIT Press, Cambridge (2001) · Zbl 0964.00020 |
| [16] | Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In Boehm, H., Flanagan, C., eds.: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, 16-19 June 2013, pp. 287-296. ACM (2013) |
| [17] | Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365-473 (2005) · Zbl 1323.68462 · doi:10.1145/1066100.1066102 |
| [18] | Goultiaeva, A., Bacchus, F.: Exploiting QBF duality on a circuit representation. In: Fox, M., Poole, D. (eds.) Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, 11-15 July 2010. AAAI Press (2010) · Zbl 1306.68158 |
| [19] | Niemetz, A., Preiner, M., Biere, A.: Turbo-charging lemmas on demand with don’t care reasoning. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21-24 October 2014, pp. 179-186. IEEE (2014) |
| [20] | Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. J. Satisfiability Boolean Model. Comput. 9, 53-58 (2014) (2015, published) |
| [21] | Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org |
| [22] | Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Automated discovery of simulation between programs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 606-621. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48899-7_42 · Zbl 1471.68061 · doi:10.1007/978-3-662-48899-7_42 |
| [23] | John, A.K., Chakraborty, S.: A layered algorithm for quantifier elimination from linear modular constraints. Formal Methods Syst. Des. 49(3), 272-323 (2016) · Zbl 1368.68332 · doi:10.1007/s10703-016-0260-9 |
| [24] | Bjørner, N., Janota, M.: Playing with quantified satisfaction. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A., (eds.) 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015. EPiC Series in Computing, Suva, Fiji, 24-28 November 2015, vol. 35, pp. 15-27. EasyChair (2015) |
| [25] | Farzan, A. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
