View in EDS

Synthesising Programs with Non-trivial Constants.

Saved in:
Bibliographic Details
Title: Synthesising Programs with Non-trivial Constants.
Authors: Abate, Alessandro1 (AUTHOR), Barbosa, Haniel2 (AUTHOR), Barrett, Clark3 (AUTHOR), David, Cristina4 (AUTHOR) cristina.david@bristol.ac.uk, Kesseli, Pascal5 (AUTHOR), Kroening, Daniel6 (AUTHOR), Polgreen, Elizabeth7 (AUTHOR), Reynolds, Andrew8 (AUTHOR), Tinelli, Cesare8 (AUTHOR)
Source: Journal of Automated Reasoning. Jun2023, Vol. 67 Issue 2, p1-25. 25p.
Abstract: Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. While useful in general, such syntactic restrictions provide little help for the generation of programs that contain non-trivial constants, unless the user is able to provide the constants in advance. This is a fundamentally difficult task for state-of-the-art synthesisers. We propose a new approach to the synthesis of programs with non-trivial constants that combines the strengths of a counterexample-guided inductive synthesiser with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T ), where T is a first-order theory. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate the practical value of CEGIS(T ) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(T ) within the mature synthesiser CVC4 and show that CEGIS(T ) improves CVC4’s results. [ABSTRACT FROM AUTHOR]
Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 163756322
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Synthesising Programs with Non-trivial Constants.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Abate%2C+Alessandro%22">Abate, Alessandro</searchLink><relatesTo>1</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Barbosa%2C+Haniel%22">Barbosa, Haniel</searchLink><relatesTo>2</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Barrett%2C+Clark%22">Barrett, Clark</searchLink><relatesTo>3</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22David%2C+Cristina%22">David, Cristina</searchLink><relatesTo>4</relatesTo> (AUTHOR)<i> cristina.david@bristol.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Kesseli%2C+Pascal%22">Kesseli, Pascal</searchLink><relatesTo>5</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Kroening%2C+Daniel%22">Kroening, Daniel</searchLink><relatesTo>6</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Polgreen%2C+Elizabeth%22">Polgreen, Elizabeth</searchLink><relatesTo>7</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Reynolds%2C+Andrew%22">Reynolds, Andrew</searchLink><relatesTo>8</relatesTo> (AUTHOR)<br /><searchLink fieldCode="AR" term="%22Tinelli%2C+Cesare%22">Tinelli, Cesare</searchLink><relatesTo>8</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Automated+Reasoning%22">Journal of Automated Reasoning</searchLink>. Jun2023, Vol. 67 Issue 2, p1-25. 25p.
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. While useful in general, such syntactic restrictions provide little help for the generation of programs that contain non-trivial constants, unless the user is able to provide the constants in advance. This is a fundamentally difficult task for state-of-the-art synthesisers. We propose a new approach to the synthesis of programs with non-trivial constants that combines the strengths of a counterexample-guided inductive synthesiser with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T ), where T is a first-order theory. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate the practical value of CEGIS(T ) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(T ) within the mature synthesiser CVC4 and show that CEGIS(T ) improves CVC4’s results. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=163756322
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10817-023-09664-4
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 25
        StartPage: 1
    Titles:
      – TitleFull: Synthesising Programs with Non-trivial Constants.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Abate, Alessandro
      – PersonEntity:
          Name:
            NameFull: Barbosa, Haniel
      – PersonEntity:
          Name:
            NameFull: Barrett, Clark
      – PersonEntity:
          Name:
            NameFull: David, Cristina
      – PersonEntity:
          Name:
            NameFull: Kesseli, Pascal
      – PersonEntity:
          Name:
            NameFull: Kroening, Daniel
      – PersonEntity:
          Name:
            NameFull: Polgreen, Elizabeth
      – PersonEntity:
          Name:
            NameFull: Reynolds, Andrew
      – PersonEntity:
          Name:
            NameFull: Tinelli, Cesare
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: Jun2023
              Type: published
              Y: 2023
          Identifiers:
            – Type: issn-print
              Value: 01687433
          Numbering:
            – Type: volume
              Value: 67
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Journal of Automated Reasoning
              Type: main
ResultId 1