×

Towards parallel Boolean functional synthesis. (English) Zbl 1452.68112

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, 337-353 (2017).
Summary: Given a relational specification \(\varphi (X, Y)\), where \(X\) and \(Y\) are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applications in several areas. In this paper, we present the first parallel approach for solving this problem, using compositional and CEGAR-style reasoning as key building blocks. We show by means of extensive experiments that our approach outperforms existing tools on a large class of benchmarks.
For the entire collection see [Zbl 1360.68015].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

sKizzo
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. 27(6), 509-516 (1978). http://dx.doi.org/10.1109/TC.1978.1675141 · Zbl 0377.94038 · doi:10.1109/TC.1978.1675141
[2] Akshay, S., Chakraborty, S., John, A., Shah, S.: Towards Parallel Boolean Functional Synthesis. ArXiv e-prints (2017). CoRR abs/1703.01440
[3] Baader, F.: On the complexity of Boolean unification. Technical report (1999) · Zbl 1338.68092
[4] Bañeres, D., Cortadella, J., Kishinevsky, M.: A recursive paradigm to solve Boolean relations. IEEE Trans. Comput. 58(4), 512-527 (2009) · Zbl 1367.94472 · doi:10.1109/TC.2008.165
[5] Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 369-376. Springer, Heidelberg (2005). doi:10.1007/11532231_27 · Zbl 1135.68550 · doi:10.1007/11532231_27
[6] Boole, G.: The Mathematical Analysis of Logic. Philosophical Library (1847). https://books.google.co.in/books?id=zv4YAQAAIAAJ · Zbl 0041.34803
[7] Boudet, A., Jouannaud, J.P., Schmidt-Schauss, M.: Unification in Boolean rings and Abelian groups. J. Symb. Comput. 8(5), 449-477 (1989). http://dx.doi.org/10.1016/S0747-7171(89)80054-9 · Zbl 0689.68040 · doi:10.1016/S0747-7171(89)80054-9
[8] Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677-691 (1986). http://dx.doi.org/10.1109/TC.1986.1676819 · Zbl 0593.94022 · doi:10.1109/TC.1986.1676819
[9] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752-794 (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643
[10] Deschamps, J.P.: Parametric solutions of Boolean equations. Discret. Math. 3(4), 333-342 (1972). http://dx.doi.org/10.1016/0012-365X(72)90090-8 · Zbl 0253.06011 · doi:10.1016/0012-365X(72)90090-8
[11] Fried, D., Tabajara, L.M., Vardi, M.Y.: BDD-based Boolean functional synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 402-421. Springer, Heidelberg (2016). doi:10.1007/978-3-319-41540-6_22 · Zbl 1411.68067 · doi:10.1007/978-3-319-41540-6_22
[12] Jiang, J.-H.R.: Quantifier elimination via functional composition. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 383-397. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_30 · Zbl 1242.68165 · doi:10.1007/978-3-642-02658-4_30
[13] Balabanov, V., Jiang, J.-H.R.: Resolution proofs and skolem functions in QBF evaluation and applications. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 149-164. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_12 · doi:10.1007/978-3-642-22110-1_12
[14] Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226-238. Springer, Heidelberg (2005). doi:10.1007/11513988_23 · Zbl 1081.68572 · doi:10.1007/11513988_23
[15] John, A., Shah, S., Chakraborty, S., Trivedi, A., Akshay, S.: Skolem functions for factored formulas. In: FMCAD, pp. 73-80 (2015)
[16] Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. CAD of Integr. Circuits Syst. 21(12), 1377-1394 (2002). http://dblp.uni-trier.de/db/journals/tcad/tcad21.html#KuehlmannPKG02 · doi:10.1109/TCAD.2002.804386
[17] Kukula, J.H., Shiple, T.R.: Building circuits from relations. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 113-123. Springer, Heidelberg (2000). doi:10.1007/10722167_12 · Zbl 0974.94502 · doi:10.1007/10722167_12
[18] Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. SIGPLAN Not. 45(6), 316-329 (2010) · doi:10.1145/1809028.1806632
[19] Logic, B., Group, V.: ABC: A System for Sequential Synthesis and Verification. http://www.eecs.berkeley.edu/ alanmi/abc/
[20] Lowenheim, L.: Über die Auflösung von Gleichungen in Logischen Gebietkalkul. Math. Ann. 68, 169-207 (1910) · JFM 41.0088.01 · doi:10.1007/BF01474159
[21] Macii, E., Odasso, G., Poncino, M.: Comparing different Boolean unification algorithms. In: Proceedings of 32nd Asilomar Conference on Signals, Systems and Computers, pp. 17-29 (2006)
[22] Marijn Heule, M.S., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Proceedings of FMCAD (2014)
[23] Martin, U., Nipkow, T.: Boolean unification - the story so far. J. Symb. Comput. 7(3-4), 275-293 (1989). http://dx.doi.org/10.1016/S0747-7171(89)80013-6 · Zbl 0682.68093 · doi:10.1016/S0747-7171(89)80013-6
[24] Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. Satisfi. Boolean Model. Comput. 9, 53-58 (2014 (published 2015))
[25] Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206-230 (1987) · Zbl 0618.93033 · doi:10.1137/0325013
[26] Akshay, S., Chakraborty, S., John, A., Shah, S.: Website for TACAS 2017 Experiments (2016). https://drive.google.com/drive/folders/0BwmvCTZAETPvVExUQkx6WVEtWWs
[27] Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, 12-15 June 2005, pp. 281-294 (2005)
[28] Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. STTT 15(5-6), 497-518 (2013) · doi:10.1007/s10009-012-0223-4
[29] Trivedi, A.: Techniques in symbolic model checking. Master’s thesis, Indian Institute of Technology Bombay, Mumbai, India (2003)
[30] Tseitin, G.
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.