Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Reports, Documentation, and Standards
  4. On Synthesis for Unbounded Bit-vector Arithmetic
 
report

On Synthesis for Unbounded Bit-vector Arithmetic

Spielmann, Andrej  
•
Kuncak, Viktor  
2012

We propose to describe computations using QFPAbit, a language of quantifier-free linear arithmetic on unbounded integers with bitvector operations. Given a QFPAbit formula with input and output variables, we describe an algo- rithm that generates an efficient linear-space function from a sequence of inputs to a sequence of outputs, without the causality restriction of reactive synthesis. The starting point for our method is a polynomial-time translation of QFPAbit into sequential circuits that check the correctness of the input/output relation. From such circuits, 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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

main.pdf

Type

Preprint

Version

http://purl.org/coar/version/c_71e4c1898caa6e32

Access type

openaccess

Size

340.99 KB

Format

Adobe PDF

Checksum (MD5)

21846bdcf399a87a2a56ea4129d9773d

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés