Abstract
We propose to describe computations using QFPAbit, a language of quantifier-free linear arithmetic on unbounded integers with bitvector operations. We describe an algorithm that, given a QFPAbit formula with input and output variables denoting integers, generates an efficient function from a sequence of inputs to a sequence of outputs, whenever such function on integers exists. The starting point for our method is a polynomial-time translation mapping a QFPAbit formula into the sequential circuit that checks the correctness of the input/output relation. From such a circuit, our synthesis algorithm produces solved circuits from inputs to outputs that are no more than singly exponential in size of the original formula. In addition to the general synthesis algorithm, we present techniques that ensure that, for example, multiplication and division with large constants do not lead to an exponential blowup, addressing a practical problem with a previous approach that used the MONA tool to generate the specification automata.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911–938 (2012)
Buchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society 138(295-311), 5 (1969)
Gupta, A.: Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. PhD thesis, CMU (1994)
Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 101–109. IEEE (2010)
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD (2006)
Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA Implementation Secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 182–194. Springer, Heidelberg (2001)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI (2010)
Rabin, M.: Automata on infinite objects and Church’s problem. Regional Conference Series in Mathematics, vol. 13. American Mathematical Society (1972)
Schuele, T., Schneider, K.: Verification of Data Paths Using Unbounded Integers: Automata Strike Back. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol. 4383, pp. 65–80. Springer, Heidelberg (2007)
Spielmann, A., Kuncak, V.: On synthesis for unbounded bit-vector arithmetic. Technical Report EPFL-REPORT-174801, EPFL (2012)
Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL (2010)
Stockmeyer, L., Meyer, A.R.: Cosmological lower bound on the circuit complexity of a small problem in logic. J. ACM 49(6), 753–784 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Spielmann, A., Kuncak, V. (2012). Synthesis for Unbounded Bit-Vector Arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_39
Download citation
DOI: https://doi.org/10.1007/978-3-642-31365-3_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31364-6
Online ISBN: 978-3-642-31365-3
eBook Packages: Computer ScienceComputer Science (R0)