View in EDS

Linear temporal constraints for sketch-based synthesizers.

Saved in:
Bibliographic Details
Title: Linear temporal constraints for sketch-based synthesizers.
Authors: Galicia-Mendoza, Fernando A.1 (AUTHOR) fernandogamen@ciencias.unam.mx, Rosenblueth, David A.2 (AUTHOR) drosenbl@unam.mx, Solar-Lezama, Armando3 (AUTHOR) asolar@csail.mit.edu
Source: Formal Methods in System Design. Jun2026, Vol. 68 Issue 3, p1-34. 34p.
Subjects: Program generators (Computer programs), Computer software, Finite state machines
Abstract: Sketch-based program synthesis allows users to guide the synthesizer by writing partial programs (sketches). Traditionally, the specifications of these sketches are safety properties expressed either as assertions or semantic equivalences. These specifications, however, lack expressiveness when the user wants to establish how the execution of the desired program evolves over time. This is especially important when synthesizing reactive programs, where the whole specification is about how the computation evolves over time. We explore an alternative method letting the user specify desired program executions as linear temporal logic (LTL) formulae. We define a method for transforming sketches with LTL assertions into sketches with only standard assertions. Specifically, for terminating programs, our method transforms and implements, within the sketch, the LTL formulae as runtime monitors. For non-terminating programs, our procedure defines and implements, into the sketch, fairness conditions (analyzing when an acceptance state of the Büchi automata equivalent to these LTL formulae occurs infinitely often). We prove the correctness of both constructions. Evaluation of our implementation in Sketch shows that our method enables the system to synthesize non-terminating programs, such as a round-robin arbiter for a variable number of devices and a lift controller for a variable number of floors. For terminating programs, our approach improves the synthesizer performance by restricting the search of program candidates without modifying the sketches structures. [ABSTRACT FROM AUTHOR]
Copyright of Formal Methods in System Design 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: 193684925
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Linear temporal constraints for sketch-based synthesizers.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Galicia-Mendoza%2C+Fernando+A%2E%22">Galicia-Mendoza, Fernando A.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> fernandogamen@ciencias.unam.mx</i><br /><searchLink fieldCode="AR" term="%22Rosenblueth%2C+David+A%2E%22">Rosenblueth, David A.</searchLink><relatesTo>2</relatesTo> (AUTHOR)<i> drosenbl@unam.mx</i><br /><searchLink fieldCode="AR" term="%22Solar-Lezama%2C+Armando%22">Solar-Lezama, Armando</searchLink><relatesTo>3</relatesTo> (AUTHOR)<i> asolar@csail.mit.edu</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Formal+Methods+in+System+Design%22">Formal Methods in System Design</searchLink>. Jun2026, Vol. 68 Issue 3, p1-34. 34p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Program+generators+%28Computer+programs%29%22">Program generators (Computer programs)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software%22">Computer software</searchLink><br /><searchLink fieldCode="DE" term="%22Finite+state+machines%22">Finite state machines</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Sketch-based program synthesis allows users to guide the synthesizer by writing partial programs (sketches). Traditionally, the specifications of these sketches are safety properties expressed either as assertions or semantic equivalences. These specifications, however, lack expressiveness when the user wants to establish how the execution of the desired program evolves over time. This is especially important when synthesizing reactive programs, where the whole specification is about how the computation evolves over time. We explore an alternative method letting the user specify desired program executions as linear temporal logic (LTL) formulae. We define a method for transforming sketches with LTL assertions into sketches with only standard assertions. Specifically, for terminating programs, our method transforms and implements, within the sketch, the LTL formulae as runtime monitors. For non-terminating programs, our procedure defines and implements, into the sketch, fairness conditions (analyzing when an acceptance state of the Büchi automata equivalent to these LTL formulae occurs infinitely often). We prove the correctness of both constructions. Evaluation of our implementation in Sketch shows that our method enables the system to synthesize non-terminating programs, such as a round-robin arbiter for a variable number of devices and a lift controller for a variable number of floors. For terminating programs, our approach improves the synthesizer performance by restricting the search of program candidates without modifying the sketches structures. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Formal Methods in System Design 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=193684925
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10703-026-00495-8
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 34
        StartPage: 1
    Subjects:
      – SubjectFull: Program generators (Computer programs)
        Type: general
      – SubjectFull: Computer software
        Type: general
      – SubjectFull: Finite state machines
        Type: general
    Titles:
      – TitleFull: Linear temporal constraints for sketch-based synthesizers.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Galicia-Mendoza, Fernando A.
      – PersonEntity:
          Name:
            NameFull: Rosenblueth, David A.
      – PersonEntity:
          Name:
            NameFull: Solar-Lezama, Armando
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: Jun2026
              Type: published
              Y: 2026
          Identifiers:
            – Type: issn-print
              Value: 09259856
          Numbering:
            – Type: volume
              Value: 68
            – Type: issue
              Value: 3
          Titles:
            – TitleFull: Formal Methods in System Design
              Type: main
ResultId 1