String Abstraction for Model Checking of C Programs View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2019-10-02

AUTHORS

Agostino Cortesi , Henrich Lauko , Martina Olliaro , Petr Ročkai

ABSTRACT

Automatic abstraction is a powerful software verification technique. In this paper, we elaborate an abstract domain for C strings, that is, null-terminated arrays of characters. We describe the abstract semantics of basic string operations and prove their soundness with regards to previously established concrete semantics of those operations. In addition to a selection of string functions from the standard C library, we provide semantics for character access and update, enabling automatic lifting of arbitrary string-manipulating code into the domain.The domain we present (called M-String) has two other abstract domains as its parameters: an index (bound) domain and a character domain. Picking different constituent domains allows M-String to be tailored for specific verification tasks, balancing precision against complexity.In addition to describing the domain theoretically, we also provide an executable implementation of the abstract operations. Using a tool which automatically lifts existing programs into the M-String domain along with an explicit-state model checker, we have evaluated the proposed domain experimentally on a few simple but realistic test programs. More... »

PAGES

74-93

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-30923-7_5

DOI

http://dx.doi.org/10.1007/978-3-030-30923-7_5

DIMENSIONS

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


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/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Ca\u2019 Foscari University, Via Torino 155, Venezia, Mestre, Italy", 
          "id": "http://www.grid.ac/institutes/grid.7240.1", 
          "name": [
            "Ca\u2019 Foscari University, Via Torino 155, Venezia, Mestre, Italy"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Cortesi", 
        "givenName": "Agostino", 
        "id": "sg:person.016321602075.60", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016321602075.60"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Lauko", 
        "givenName": "Henrich", 
        "id": "sg:person.010156102043.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Ca\u2019 Foscari University, Via Torino 155, Venezia, Mestre, Italy", 
          "id": "http://www.grid.ac/institutes/grid.7240.1", 
          "name": [
            "Ca\u2019 Foscari University, Via Torino 155, Venezia, Mestre, Italy"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Olliaro", 
        "givenName": "Martina", 
        "id": "sg:person.011130417507.72", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011130417507.72"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ro\u010dkai", 
        "givenName": "Petr", 
        "id": "sg:person.07377571657.86", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2019-10-02", 
    "datePublishedReg": "2019-10-02", 
    "description": "Automatic abstraction is a powerful software verification technique. In this paper, we elaborate an abstract domain for C strings, that is, null-terminated arrays of characters. We describe the abstract semantics of basic string operations and prove their soundness with regards to previously established concrete semantics of those operations. In addition to a selection of string functions from the standard C library, we provide semantics for character access and update, enabling automatic lifting of arbitrary string-manipulating code into the domain.The domain we present (called M-String) has two other abstract domains as its parameters: an index (bound) domain and a character domain. Picking different constituent domains allows M-String to be tailored for specific verification tasks, balancing precision against complexity.In addition to describing the domain theoretically, we also provide an executable implementation of the abstract operations. Using a tool which automatically lifts existing programs into the M-String domain along with an explicit-state model checker, we have evaluated the proposed domain experimentally on a few simple but realistic test programs.", 
    "editor": [
      {
        "familyName": "Biondi", 
        "givenName": "Fabrizio", 
        "type": "Person"
      }, 
      {
        "familyName": "Given-Wilson", 
        "givenName": "Thomas", 
        "type": "Person"
      }, 
      {
        "familyName": "Legay", 
        "givenName": "Axel", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-30923-7_5", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-030-30922-0", 
        "978-3-030-30923-7"
      ], 
      "name": "Model Checking Software", 
      "type": "Book"
    }, 
    "keywords": [
      "abstract domain", 
      "explicit-state model checker", 
      "software verification techniques", 
      "specific verification tasks", 
      "standard C library", 
      "automatic abstraction", 
      "executable implementation", 
      "model checker", 
      "verification techniques", 
      "C library", 
      "model checking", 
      "C-string", 
      "C programs", 
      "abstract semantics", 
      "concrete semantics", 
      "string operations", 
      "abstract operations", 
      "verification task", 
      "automatic lifting", 
      "semantics", 
      "character domains", 
      "abstraction", 
      "index domain", 
      "string functions", 
      "checker", 
      "checking", 
      "domain", 
      "operation", 
      "task", 
      "test program", 
      "complexity", 
      "implementation", 
      "code", 
      "soundness", 
      "constituent domains", 
      "M-strings", 
      "library", 
      "update", 
      "access", 
      "tool", 
      "precision", 
      "string", 
      "program", 
      "technique", 
      "selection", 
      "array", 
      "addition", 
      "parameters", 
      "lifting", 
      "function", 
      "regard", 
      "character", 
      "paper"
    ], 
    "name": "String Abstraction for Model Checking of C Programs", 
    "pagination": "74-93", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1121429575"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-30923-7_5"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-30923-7_5", 
      "https://app.dimensions.ai/details/publication/pub.1121429575"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:20", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220804/entities/gbq_results/chapter/chapter_427.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-30923-7_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/978-3-030-30923-7_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/978-3-030-30923-7_5'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-30923-7_5'

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-030-30923-7_5'


 

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

150 TRIPLES      22 PREDICATES      78 URIs      70 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-30923-7_5 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0803
4 schema:author N56e9523acae94980ad5758a637e9f440
5 schema:datePublished 2019-10-02
6 schema:datePublishedReg 2019-10-02
7 schema:description Automatic abstraction is a powerful software verification technique. In this paper, we elaborate an abstract domain for C strings, that is, null-terminated arrays of characters. We describe the abstract semantics of basic string operations and prove their soundness with regards to previously established concrete semantics of those operations. In addition to a selection of string functions from the standard C library, we provide semantics for character access and update, enabling automatic lifting of arbitrary string-manipulating code into the domain.The domain we present (called M-String) has two other abstract domains as its parameters: an index (bound) domain and a character domain. Picking different constituent domains allows M-String to be tailored for specific verification tasks, balancing precision against complexity.In addition to describing the domain theoretically, we also provide an executable implementation of the abstract operations. Using a tool which automatically lifts existing programs into the M-String domain along with an explicit-state model checker, we have evaluated the proposed domain experimentally on a few simple but realistic test programs.
8 schema:editor N6d665ebfffb043a7a9843e256d5a975d
9 schema:genre chapter
10 schema:isAccessibleForFree true
11 schema:isPartOf N25260e68398c4f67a58f551c9f52bf00
12 schema:keywords C library
13 C programs
14 C-string
15 M-strings
16 abstract domain
17 abstract operations
18 abstract semantics
19 abstraction
20 access
21 addition
22 array
23 automatic abstraction
24 automatic lifting
25 character
26 character domains
27 checker
28 checking
29 code
30 complexity
31 concrete semantics
32 constituent domains
33 domain
34 executable implementation
35 explicit-state model checker
36 function
37 implementation
38 index domain
39 library
40 lifting
41 model checker
42 model checking
43 operation
44 paper
45 parameters
46 precision
47 program
48 regard
49 selection
50 semantics
51 software verification techniques
52 soundness
53 specific verification tasks
54 standard C library
55 string
56 string functions
57 string operations
58 task
59 technique
60 test program
61 tool
62 update
63 verification task
64 verification techniques
65 schema:name String Abstraction for Model Checking of C Programs
66 schema:pagination 74-93
67 schema:productId N256766b8c3a743c6a7de5feee41d672c
68 N51eaeed4e71b49d6bb7ede1f7eefe995
69 schema:publisher N2ea77e3dff054f858403b69a2d8c7032
70 schema:sameAs https://app.dimensions.ai/details/publication/pub.1121429575
71 https://doi.org/10.1007/978-3-030-30923-7_5
72 schema:sdDatePublished 2022-08-04T17:20
73 schema:sdLicense https://scigraph.springernature.com/explorer/license/
74 schema:sdPublisher N62522ae2ada4436cbf6ebdcfe19d1d15
75 schema:url https://doi.org/10.1007/978-3-030-30923-7_5
76 sgo:license sg:explorer/license/
77 sgo:sdDataset chapters
78 rdf:type schema:Chapter
79 N09fda877512e4c39859db429e222e2c5 rdf:first N31304bc62ffb409cbefa2955316d460d
80 rdf:rest rdf:nil
81 N25260e68398c4f67a58f551c9f52bf00 schema:isbn 978-3-030-30922-0
82 978-3-030-30923-7
83 schema:name Model Checking Software
84 rdf:type schema:Book
85 N256766b8c3a743c6a7de5feee41d672c schema:name doi
86 schema:value 10.1007/978-3-030-30923-7_5
87 rdf:type schema:PropertyValue
88 N26a359fb99a4498981b6d1984aa3823d schema:familyName Biondi
89 schema:givenName Fabrizio
90 rdf:type schema:Person
91 N2ea77e3dff054f858403b69a2d8c7032 schema:name Springer Nature
92 rdf:type schema:Organisation
93 N31304bc62ffb409cbefa2955316d460d schema:familyName Legay
94 schema:givenName Axel
95 rdf:type schema:Person
96 N4f19ef5127cf4f38aa97b2f489c7ba40 rdf:first sg:person.07377571657.86
97 rdf:rest rdf:nil
98 N51eaeed4e71b49d6bb7ede1f7eefe995 schema:name dimensions_id
99 schema:value pub.1121429575
100 rdf:type schema:PropertyValue
101 N56e9523acae94980ad5758a637e9f440 rdf:first sg:person.016321602075.60
102 rdf:rest Na699189891a4463bbf2ef65b6e87ea35
103 N62522ae2ada4436cbf6ebdcfe19d1d15 schema:name Springer Nature - SN SciGraph project
104 rdf:type schema:Organization
105 N6d665ebfffb043a7a9843e256d5a975d rdf:first N26a359fb99a4498981b6d1984aa3823d
106 rdf:rest Nb1d9aa5fd0a4450c9507dc193e85cdf6
107 Na699189891a4463bbf2ef65b6e87ea35 rdf:first sg:person.010156102043.29
108 rdf:rest Ne80471ab2fb844b4865cdb4936fdb20d
109 Nb1d9aa5fd0a4450c9507dc193e85cdf6 rdf:first Nd8209c8edf1c4639bb3ea8d514b511b4
110 rdf:rest N09fda877512e4c39859db429e222e2c5
111 Nd8209c8edf1c4639bb3ea8d514b511b4 schema:familyName Given-Wilson
112 schema:givenName Thomas
113 rdf:type schema:Person
114 Ne80471ab2fb844b4865cdb4936fdb20d rdf:first sg:person.011130417507.72
115 rdf:rest N4f19ef5127cf4f38aa97b2f489c7ba40
116 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
117 schema:name Information and Computing Sciences
118 rdf:type schema:DefinedTerm
119 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
120 schema:name Artificial Intelligence and Image Processing
121 rdf:type schema:DefinedTerm
122 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
123 schema:name Computer Software
124 rdf:type schema:DefinedTerm
125 sg:person.010156102043.29 schema:affiliation grid-institutes:grid.10267.32
126 schema:familyName Lauko
127 schema:givenName Henrich
128 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29
129 rdf:type schema:Person
130 sg:person.011130417507.72 schema:affiliation grid-institutes:grid.7240.1
131 schema:familyName Olliaro
132 schema:givenName Martina
133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011130417507.72
134 rdf:type schema:Person
135 sg:person.016321602075.60 schema:affiliation grid-institutes:grid.7240.1
136 schema:familyName Cortesi
137 schema:givenName Agostino
138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016321602075.60
139 rdf:type schema:Person
140 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
141 schema:familyName Ročkai
142 schema:givenName Petr
143 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
144 rdf:type schema:Person
145 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
146 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
147 rdf:type schema:Organization
148 grid-institutes:grid.7240.1 schema:alternateName Ca’ Foscari University, Via Torino 155, Venezia, Mestre, Italy
149 schema:name Ca’ Foscari University, Via Torino 155, Venezia, Mestre, Italy
150 rdf:type schema:Organization
 




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


...