Combining techniques of bounded model checking and constraint programming to aid for error localization View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2017-01

AUTHORS

Mohammed Bekkouche

ABSTRACT

A model checker can produce a trace of counter-example for erroneous program, which is often difficult to exploit to locate errors in source code. In my thesis, we proposed an error localization algorithm from counter-examples, named LocFaults, combining approaches of Bounded Model-Checking (BMC) with constraint satisfaction problem (CSP). This algorithm analyzes the paths of CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of control flow graph for which at most k conditional statements can be wrong. Then we calculate the MCSs (Minimal Correction Sets) of limited size on each of these paths. Removal of one of these sets of constraints gives a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the postcondition. To calculate the MCSs, we extend the generic algorithm proposed by Liffiton and Sakallah in order to deal with programs with numerical instructions more efficiently. This approach has been experimentally evaluated on a set of academic and realistic programs. More... »

PAGES

93-94

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/s10601-016-9259-5

DOI

http://dx.doi.org/10.1007/s10601-016-9259-5

DIMENSIONS

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


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/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Nice Sophia Antipolis University", 
          "id": "https://www.grid.ac/institutes/grid.10737.32", 
          "name": [
            "University of Nice Sophia Antipolis, Nice, France"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Bekkouche", 
        "givenName": "Mohammed", 
        "id": "sg:person.016231104051.30", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016231104051.30"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2017-01", 
    "datePublishedReg": "2017-01-01", 
    "description": "A model checker can produce a trace of counter-example for erroneous program, which is often difficult to exploit to locate errors in source code. In my thesis, we proposed an error localization algorithm from counter-examples, named LocFaults, combining approaches of Bounded Model-Checking (BMC) with constraint satisfaction problem (CSP). This algorithm analyzes the paths of CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of control flow graph for which at most k conditional statements can be wrong. Then we calculate the MCSs (Minimal Correction Sets) of limited size on each of these paths. Removal of one of these sets of constraints gives a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the postcondition. To calculate the MCSs, we extend the generic algorithm proposed by Liffiton and Sakallah in order to deal with programs with numerical instructions more efficiently. This approach has been experimentally evaluated on a set of academic and realistic programs.", 
    "genre": "non_research_article", 
    "id": "sg:pub.10.1007/s10601-016-9259-5", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": true, 
    "isPartOf": [
      {
        "id": "sg:journal.1043977", 
        "issn": [
          "1383-7133", 
          "1572-9354"
        ], 
        "name": "Constraints", 
        "type": "Periodical"
      }, 
      {
        "issueNumber": "1", 
        "type": "PublicationIssue"
      }, 
      {
        "type": "PublicationVolume", 
        "volumeNumber": "22"
      }
    ], 
    "name": "Combining techniques of bounded model checking and constraint programming to aid for error localization", 
    "pagination": "93-94", 
    "productId": [
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "199d18b91f43aefe333112da90be051f08f140432acf0007d1c1c2870a9c1fd9"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/s10601-016-9259-5"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1005376197"
        ]
      }
    ], 
    "sameAs": [
      "https://doi.org/10.1007/s10601-016-9259-5", 
      "https://app.dimensions.ai/details/publication/pub.1005376197"
    ], 
    "sdDataset": "articles", 
    "sdDatePublished": "2019-04-11T12:25", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000362_0000000362/records_87104_00000000.jsonl", 
    "type": "ScholarlyArticle", 
    "url": "https://link.springer.com/10.1007%2Fs10601-016-9259-5"
  }
]
 

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/s10601-016-9259-5'

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/s10601-016-9259-5'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10601-016-9259-5'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10601-016-9259-5'


 

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

61 TRIPLES      20 PREDICATES      27 URIs      19 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/s10601-016-9259-5 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N2788903f04b549b6a7242c97a5e6c608
4 schema:datePublished 2017-01
5 schema:datePublishedReg 2017-01-01
6 schema:description A model checker can produce a trace of counter-example for erroneous program, which is often difficult to exploit to locate errors in source code. In my thesis, we proposed an error localization algorithm from counter-examples, named LocFaults, combining approaches of Bounded Model-Checking (BMC) with constraint satisfaction problem (CSP). This algorithm analyzes the paths of CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of control flow graph for which at most k conditional statements can be wrong. Then we calculate the MCSs (Minimal Correction Sets) of limited size on each of these paths. Removal of one of these sets of constraints gives a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the postcondition. To calculate the MCSs, we extend the generic algorithm proposed by Liffiton and Sakallah in order to deal with programs with numerical instructions more efficiently. This approach has been experimentally evaluated on a set of academic and realistic programs.
7 schema:genre non_research_article
8 schema:inLanguage en
9 schema:isAccessibleForFree true
10 schema:isPartOf Ne8965178cbce49688a6ea5cd5c1c227a
11 Ned2032bedcb449a983962f94cc685ebf
12 sg:journal.1043977
13 schema:name Combining techniques of bounded model checking and constraint programming to aid for error localization
14 schema:pagination 93-94
15 schema:productId Na70daac12ecf4ac787d5f726a88804cd
16 Nee3ddb57628f4756915bc2c335709f8b
17 Nf52a097abee14a5184eb1bc934ebe50c
18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005376197
19 https://doi.org/10.1007/s10601-016-9259-5
20 schema:sdDatePublished 2019-04-11T12:25
21 schema:sdLicense https://scigraph.springernature.com/explorer/license/
22 schema:sdPublisher N0ef7c6e52c9942c8a796861ccc4a6c7a
23 schema:url https://link.springer.com/10.1007%2Fs10601-016-9259-5
24 sgo:license sg:explorer/license/
25 sgo:sdDataset articles
26 rdf:type schema:ScholarlyArticle
27 N0ef7c6e52c9942c8a796861ccc4a6c7a schema:name Springer Nature - SN SciGraph project
28 rdf:type schema:Organization
29 N2788903f04b549b6a7242c97a5e6c608 rdf:first sg:person.016231104051.30
30 rdf:rest rdf:nil
31 Na70daac12ecf4ac787d5f726a88804cd schema:name doi
32 schema:value 10.1007/s10601-016-9259-5
33 rdf:type schema:PropertyValue
34 Ne8965178cbce49688a6ea5cd5c1c227a schema:issueNumber 1
35 rdf:type schema:PublicationIssue
36 Ned2032bedcb449a983962f94cc685ebf schema:volumeNumber 22
37 rdf:type schema:PublicationVolume
38 Nee3ddb57628f4756915bc2c335709f8b schema:name readcube_id
39 schema:value 199d18b91f43aefe333112da90be051f08f140432acf0007d1c1c2870a9c1fd9
40 rdf:type schema:PropertyValue
41 Nf52a097abee14a5184eb1bc934ebe50c schema:name dimensions_id
42 schema:value pub.1005376197
43 rdf:type schema:PropertyValue
44 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
45 schema:name Information and Computing Sciences
46 rdf:type schema:DefinedTerm
47 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
48 schema:name Computation Theory and Mathematics
49 rdf:type schema:DefinedTerm
50 sg:journal.1043977 schema:issn 1383-7133
51 1572-9354
52 schema:name Constraints
53 rdf:type schema:Periodical
54 sg:person.016231104051.30 schema:affiliation https://www.grid.ac/institutes/grid.10737.32
55 schema:familyName Bekkouche
56 schema:givenName Mohammed
57 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016231104051.30
58 rdf:type schema:Person
59 https://www.grid.ac/institutes/grid.10737.32 schema:alternateName Nice Sophia Antipolis University
60 schema:name University of Nice Sophia Antipolis, Nice, France
61 rdf:type schema:Organization
 




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


...