Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2017-03-31

AUTHORS

ThanhVu Nguyen , Westley Weimer , Deepak Kapur , Stephanie Forrest

ABSTRACT

We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for the transfer of techniques and results between them.To demonstrate the equivalence, we develop a program repair prototype using reachability tools. We transform a buggy program and its required specification into a specific program containing a location reachable only when the original program can be repaired, and then apply an off-the-shelf test-input generation tool on the transformed program to find test values to reach the desired location. Those test values correspond to repairs for the original program. Preliminary results suggest that our approach compares favorably to other repair methods. More... »

PAGES

301-318

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-662-54576-8
978-3-662-54577-5

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-54577-5_17

DOI

http://dx.doi.org/10.1007/978-3-662-54577-5_17

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1084715006


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/03", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Chemical Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0305", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Organic Chemistry", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "University of Nebraska, Lincoln, Nebraska, USA", 
          "id": "http://www.grid.ac/institutes/grid.24434.35", 
          "name": [
            "University of Nebraska, Lincoln, Nebraska, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Nguyen", 
        "givenName": "ThanhVu", 
        "id": "sg:person.012435420235.40", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012435420235.40"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Virginia, Charlottesville, Virginia, USA", 
          "id": "http://www.grid.ac/institutes/grid.27755.32", 
          "name": [
            "University of Virginia, Charlottesville, Virginia, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Weimer", 
        "givenName": "Westley", 
        "id": "sg:person.014010553007.40", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014010553007.40"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of New Mexico, Albuquerque, New Mexico, USA", 
          "id": "http://www.grid.ac/institutes/grid.266832.b", 
          "name": [
            "University of New Mexico, Albuquerque, New Mexico, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kapur", 
        "givenName": "Deepak", 
        "id": "sg:person.01127144134.28", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01127144134.28"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of New Mexico, Albuquerque, New Mexico, USA", 
          "id": "http://www.grid.ac/institutes/grid.266832.b", 
          "name": [
            "University of New Mexico, Albuquerque, New Mexico, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Forrest", 
        "givenName": "Stephanie", 
        "id": "sg:person.0712103012.64", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0712103012.64"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2017-03-31", 
    "datePublishedReg": "2017-03-31", 
    "description": "We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for the transfer of techniques and results between them.To demonstrate the equivalence, we develop a program repair prototype using reachability tools. We transform a buggy program and its required specification into a specific program containing a location reachable only when the original program can be repaired, and then apply an off-the-shelf test-input generation tool on the transformed program to find test values to reach the desired location. Those test values correspond to repairs for the original program. Preliminary results suggest that our approach compares favorably to other repair methods.", 
    "editor": [
      {
        "familyName": "Legay", 
        "givenName": "Axel", 
        "type": "Person"
      }, 
      {
        "familyName": "Margaria", 
        "givenName": "Tiziana", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-54577-5_17", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-662-54576-8", 
        "978-3-662-54577-5"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "program synthesis", 
      "test-input generation", 
      "original program", 
      "generation tool", 
      "buggy programs", 
      "reachability tools", 
      "transfer of techniques", 
      "reachability problem", 
      "program location", 
      "reachability", 
      "constructive proof", 
      "research field", 
      "synthesis problem", 
      "pre-specified forms", 
      "tool", 
      "specification", 
      "preliminary results", 
      "prototype", 
      "location", 
      "program", 
      "proof", 
      "repair method", 
      "specific programs", 
      "technique", 
      "link", 
      "method", 
      "results", 
      "generation", 
      "equivalence", 
      "field", 
      "formulation", 
      "values", 
      "form", 
      "transfer", 
      "reduction", 
      "test values", 
      "synthesis", 
      "certain formulations", 
      "repair", 
      "problem", 
      "approach", 
      "template-based synthesis problem", 
      "program repair prototype", 
      "repair prototype", 
      "shelf test-input generation tool", 
      "test-input generation tool", 
      "Automatic Program Repair Using Test-Input Generation", 
      "Program Repair Using Test-Input Generation", 
      "Repair Using Test-Input Generation", 
      "Using Test-Input Generation"
    ], 
    "name": "Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation", 
    "pagination": "301-318", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1084715006"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-54577-5_17"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-54577-5_17", 
      "https://app.dimensions.ai/details/publication/pub.1084715006"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:07", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_369.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-662-54577-5_17"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-54577-5_17'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-54577-5_17'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-54577-5_17'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-54577-5_17'


 

This table displays all metadata directly associated to this object as RDF triples.

142 TRIPLES      23 PREDICATES      75 URIs      68 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-54577-5_17 schema:about anzsrc-for:03
2 anzsrc-for:0305
3 schema:author Nd87c47cc30914284bef3e38fd1e17704
4 schema:datePublished 2017-03-31
5 schema:datePublishedReg 2017-03-31
6 schema:description We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for the transfer of techniques and results between them.To demonstrate the equivalence, we develop a program repair prototype using reachability tools. We transform a buggy program and its required specification into a specific program containing a location reachable only when the original program can be repaired, and then apply an off-the-shelf test-input generation tool on the transformed program to find test values to reach the desired location. Those test values correspond to repairs for the original program. Preliminary results suggest that our approach compares favorably to other repair methods.
7 schema:editor N762ec54411814e63bfabc01d2aeddea0
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N2e100d7b95f94e0c8fd2a9634b59eebf
12 schema:keywords Automatic Program Repair Using Test-Input Generation
13 Program Repair Using Test-Input Generation
14 Repair Using Test-Input Generation
15 Using Test-Input Generation
16 approach
17 buggy programs
18 certain formulations
19 constructive proof
20 equivalence
21 field
22 form
23 formulation
24 generation
25 generation tool
26 link
27 location
28 method
29 original program
30 pre-specified forms
31 preliminary results
32 problem
33 program
34 program location
35 program repair prototype
36 program synthesis
37 proof
38 prototype
39 reachability
40 reachability problem
41 reachability tools
42 reduction
43 repair
44 repair method
45 repair prototype
46 research field
47 results
48 shelf test-input generation tool
49 specific programs
50 specification
51 synthesis
52 synthesis problem
53 technique
54 template-based synthesis problem
55 test values
56 test-input generation
57 test-input generation tool
58 tool
59 transfer
60 transfer of techniques
61 values
62 schema:name Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
63 schema:pagination 301-318
64 schema:productId N5ae2e6a8529c448da1788499fdc5d9d1
65 N8ed1e6a44cfd42dab159f734109eb456
66 schema:publisher Nc6938181bd72433ba950182fef2ba38e
67 schema:sameAs https://app.dimensions.ai/details/publication/pub.1084715006
68 https://doi.org/10.1007/978-3-662-54577-5_17
69 schema:sdDatePublished 2021-12-01T20:07
70 schema:sdLicense https://scigraph.springernature.com/explorer/license/
71 schema:sdPublisher Ncbf158223c3946b7b2aebe318f3ae615
72 schema:url https://doi.org/10.1007/978-3-662-54577-5_17
73 sgo:license sg:explorer/license/
74 sgo:sdDataset chapters
75 rdf:type schema:Chapter
76 N01f4d5ceb905434b90d83ac0482a5591 schema:familyName Margaria
77 schema:givenName Tiziana
78 rdf:type schema:Person
79 N2e100d7b95f94e0c8fd2a9634b59eebf schema:isbn 978-3-662-54576-8
80 978-3-662-54577-5
81 schema:name Tools and Algorithms for the Construction and Analysis of Systems
82 rdf:type schema:Book
83 N3d915cdf56c14b6cb9c2990df8018d5f schema:familyName Legay
84 schema:givenName Axel
85 rdf:type schema:Person
86 N45167f0a4d9f49f29758b2ff7e102c34 rdf:first N01f4d5ceb905434b90d83ac0482a5591
87 rdf:rest rdf:nil
88 N5ae2e6a8529c448da1788499fdc5d9d1 schema:name dimensions_id
89 schema:value pub.1084715006
90 rdf:type schema:PropertyValue
91 N5f8e271704424252b8a796f8d7aca8b4 rdf:first sg:person.014010553007.40
92 rdf:rest Nd7e025c4d99047ae8dd399884c01f906
93 N762ec54411814e63bfabc01d2aeddea0 rdf:first N3d915cdf56c14b6cb9c2990df8018d5f
94 rdf:rest N45167f0a4d9f49f29758b2ff7e102c34
95 N8ed1e6a44cfd42dab159f734109eb456 schema:name doi
96 schema:value 10.1007/978-3-662-54577-5_17
97 rdf:type schema:PropertyValue
98 N949e596f2e8f4860b19cdb46bb09febc rdf:first sg:person.0712103012.64
99 rdf:rest rdf:nil
100 Nc6938181bd72433ba950182fef2ba38e schema:name Springer Nature
101 rdf:type schema:Organisation
102 Ncbf158223c3946b7b2aebe318f3ae615 schema:name Springer Nature - SN SciGraph project
103 rdf:type schema:Organization
104 Nd7e025c4d99047ae8dd399884c01f906 rdf:first sg:person.01127144134.28
105 rdf:rest N949e596f2e8f4860b19cdb46bb09febc
106 Nd87c47cc30914284bef3e38fd1e17704 rdf:first sg:person.012435420235.40
107 rdf:rest N5f8e271704424252b8a796f8d7aca8b4
108 anzsrc-for:03 schema:inDefinedTermSet anzsrc-for:
109 schema:name Chemical Sciences
110 rdf:type schema:DefinedTerm
111 anzsrc-for:0305 schema:inDefinedTermSet anzsrc-for:
112 schema:name Organic Chemistry
113 rdf:type schema:DefinedTerm
114 sg:person.01127144134.28 schema:affiliation grid-institutes:grid.266832.b
115 schema:familyName Kapur
116 schema:givenName Deepak
117 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01127144134.28
118 rdf:type schema:Person
119 sg:person.012435420235.40 schema:affiliation grid-institutes:grid.24434.35
120 schema:familyName Nguyen
121 schema:givenName ThanhVu
122 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012435420235.40
123 rdf:type schema:Person
124 sg:person.014010553007.40 schema:affiliation grid-institutes:grid.27755.32
125 schema:familyName Weimer
126 schema:givenName Westley
127 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014010553007.40
128 rdf:type schema:Person
129 sg:person.0712103012.64 schema:affiliation grid-institutes:grid.266832.b
130 schema:familyName Forrest
131 schema:givenName Stephanie
132 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0712103012.64
133 rdf:type schema:Person
134 grid-institutes:grid.24434.35 schema:alternateName University of Nebraska, Lincoln, Nebraska, USA
135 schema:name University of Nebraska, Lincoln, Nebraska, USA
136 rdf:type schema:Organization
137 grid-institutes:grid.266832.b schema:alternateName University of New Mexico, Albuquerque, New Mexico, USA
138 schema:name University of New Mexico, Albuquerque, New Mexico, USA
139 rdf:type schema:Organization
140 grid-institutes:grid.27755.32 schema:alternateName University of Virginia, Charlottesville, Virginia, USA
141 schema:name University of Virginia, Charlottesville, Virginia, USA
142 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...