Verification of Certifying Computations through AutoCorres and Simpl View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2014

AUTHORS

Lars Noschinski , Christine Rizkallah , Kurt Mehlhorn

ABSTRACT

Certifying algorithms compute not only an output, but also a witness that certifies the correctness of the output for a particular input. A checker program uses this certificate to ascertain the correctness of the output. Recent work used the verification tools VCC and Isabelle to verify checker implementations and their mathematical background theory. The checkers verified stem from the widely-used algorithms library LEDA and are written in C. The drawback of this approach is the use of two different tools. The advantage is that it could be carried out with reasonable effort in 2011. In this article, we evaluate the feasibility of performing the entire verification within Isabelle. For this purpose, we consider checkers written in the imperative languages C and Simpl. We re-verify the checker for connectedness of graphs and present a verification of the LEDA checker for non-planarity of graphs. For the checkers written in C, we translate from C to Isabelle using the AutoCorres tool set and then reason in Isabelle. For the checkers written in Simpl, Isabelle is the only tool needed. We compare the new approach with the previous approach and discuss advantages and disadvantages. We conclude that the new approach provides higher trust guarantees and it is particularly promising for checkers that require domain-specific reasoning. More... »

PAGES

46-61

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-06200-6_4

DOI

http://dx.doi.org/10.1007/978-3-319-06200-6_4

DIMENSIONS

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


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/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany", 
          "id": "http://www.grid.ac/institutes/grid.6936.a", 
          "name": [
            "Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Noschinski", 
        "givenName": "Lars", 
        "id": "sg:person.011500152103.44", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011500152103.44"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany", 
          "id": "http://www.grid.ac/institutes/grid.6936.a", 
          "name": [
            "Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Rizkallah", 
        "givenName": "Christine", 
        "id": "sg:person.010574656021.33", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010574656021.33"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany", 
          "id": "http://www.grid.ac/institutes/grid.419528.3", 
          "name": [
            "Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Mehlhorn", 
        "givenName": "Kurt", 
        "id": "sg:person.011757371347.43", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011757371347.43"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2014", 
    "datePublishedReg": "2014-01-01", 
    "description": "Certifying algorithms compute not only an output, but also a witness that certifies the correctness of the output for a particular input. A checker program uses this certificate to ascertain the correctness of the output. Recent work used the verification tools VCC and Isabelle to verify checker implementations and their mathematical background theory. The checkers verified stem from the widely-used algorithms library LEDA and are written in C. The drawback of this approach is the use of two different tools. The advantage is that it could be carried out with reasonable effort in 2011. In this article, we evaluate the feasibility of performing the entire verification within Isabelle. For this purpose, we consider checkers written in the imperative languages C and Simpl. We re-verify the checker for connectedness of graphs and present a verification of the LEDA checker for non-planarity of graphs. For the checkers written in C, we translate from C to Isabelle using the AutoCorres tool set and then reason in Isabelle. For the checkers written in Simpl, Isabelle is the only tool needed. We compare the new approach with the previous approach and discuss advantages and disadvantages. We conclude that the new approach provides higher trust guarantees and it is particularly promising for checkers that require domain-specific reasoning.", 
    "editor": [
      {
        "familyName": "Badger", 
        "givenName": "Julia M.", 
        "type": "Person"
      }, 
      {
        "familyName": "Rozier", 
        "givenName": "Kristin Yvonne", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-06200-6_4", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-06199-3", 
        "978-3-319-06200-6"
      ], 
      "name": "NASA Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "domain-specific reasoning", 
      "connectedness of graphs", 
      "trust guarantees", 
      "entire verification", 
      "language C", 
      "checker", 
      "checkers program", 
      "new approach", 
      "previous approaches", 
      "Isabelle", 
      "different tools", 
      "reasonable effort", 
      "particular input", 
      "verification", 
      "SIMPL", 
      "correctness", 
      "graph", 
      "background theory", 
      "tool", 
      "algorithm", 
      "guarantees", 
      "computation", 
      "reasoning", 
      "only tool", 
      "recent work", 
      "advantages", 
      "implementation", 
      "output", 
      "LEDA", 
      "drawbacks", 
      "certificates", 
      "input", 
      "VCC", 
      "feasibility", 
      "work", 
      "disadvantages", 
      "efforts", 
      "program", 
      "use", 
      "purpose", 
      "connectedness", 
      "article", 
      "reasons", 
      "theory", 
      "witness", 
      "approach"
    ], 
    "name": "Verification of Certifying Computations through AutoCorres and Simpl", 
    "pagination": "46-61", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1042087635"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-06200-6_4"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-06200-6_4", 
      "https://app.dimensions.ai/details/publication/pub.1042087635"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-10-01T06:54", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20221001/entities/gbq_results/chapter/chapter_221.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-06200-6_4"
  }
]
 

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-319-06200-6_4'

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-319-06200-6_4'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-06200-6_4'

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-319-06200-6_4'


 

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

127 TRIPLES      22 PREDICATES      71 URIs      64 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-06200-6_4 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N14cbc8919f9b4276ad376ac079f647fd
4 schema:datePublished 2014
5 schema:datePublishedReg 2014-01-01
6 schema:description Certifying algorithms compute not only an output, but also a witness that certifies the correctness of the output for a particular input. A checker program uses this certificate to ascertain the correctness of the output. Recent work used the verification tools VCC and Isabelle to verify checker implementations and their mathematical background theory. The checkers verified stem from the widely-used algorithms library LEDA and are written in C. The drawback of this approach is the use of two different tools. The advantage is that it could be carried out with reasonable effort in 2011. In this article, we evaluate the feasibility of performing the entire verification within Isabelle. For this purpose, we consider checkers written in the imperative languages C and Simpl. We re-verify the checker for connectedness of graphs and present a verification of the LEDA checker for non-planarity of graphs. For the checkers written in C, we translate from C to Isabelle using the AutoCorres tool set and then reason in Isabelle. For the checkers written in Simpl, Isabelle is the only tool needed. We compare the new approach with the previous approach and discuss advantages and disadvantages. We conclude that the new approach provides higher trust guarantees and it is particularly promising for checkers that require domain-specific reasoning.
7 schema:editor N2e64438bfe5e4703b9ad44c1b1cd22e4
8 schema:genre chapter
9 schema:isAccessibleForFree false
10 schema:isPartOf N75d2cf07b61149b8b673ae9d30cbd501
11 schema:keywords Isabelle
12 LEDA
13 SIMPL
14 VCC
15 advantages
16 algorithm
17 approach
18 article
19 background theory
20 certificates
21 checker
22 checkers program
23 computation
24 connectedness
25 connectedness of graphs
26 correctness
27 different tools
28 disadvantages
29 domain-specific reasoning
30 drawbacks
31 efforts
32 entire verification
33 feasibility
34 graph
35 guarantees
36 implementation
37 input
38 language C
39 new approach
40 only tool
41 output
42 particular input
43 previous approaches
44 program
45 purpose
46 reasonable effort
47 reasoning
48 reasons
49 recent work
50 theory
51 tool
52 trust guarantees
53 use
54 verification
55 witness
56 work
57 schema:name Verification of Certifying Computations through AutoCorres and Simpl
58 schema:pagination 46-61
59 schema:productId N74c31c755d294bfb80cc9855713e5705
60 Nd3d53b3e8abc46e5963f9a568f09aefc
61 schema:publisher N5f21ffd819a3484caa217d0cd2972467
62 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042087635
63 https://doi.org/10.1007/978-3-319-06200-6_4
64 schema:sdDatePublished 2022-10-01T06:54
65 schema:sdLicense https://scigraph.springernature.com/explorer/license/
66 schema:sdPublisher N935e2c8256b3459c9656f32233621bbb
67 schema:url https://doi.org/10.1007/978-3-319-06200-6_4
68 sgo:license sg:explorer/license/
69 sgo:sdDataset chapters
70 rdf:type schema:Chapter
71 N0a125535dc7a4192a09f6bdaa18e2ec3 rdf:first sg:person.010574656021.33
72 rdf:rest N2a1ed961e64e4947be0a0af23b1da6d0
73 N14cbc8919f9b4276ad376ac079f647fd rdf:first sg:person.011500152103.44
74 rdf:rest N0a125535dc7a4192a09f6bdaa18e2ec3
75 N2a1ed961e64e4947be0a0af23b1da6d0 rdf:first sg:person.011757371347.43
76 rdf:rest rdf:nil
77 N2e64438bfe5e4703b9ad44c1b1cd22e4 rdf:first Nbdaf447efa7b4b01a729968654be1926
78 rdf:rest Nceac301110d84c9999c22d82f5f9931b
79 N5f21ffd819a3484caa217d0cd2972467 schema:name Springer Nature
80 rdf:type schema:Organisation
81 N74c31c755d294bfb80cc9855713e5705 schema:name doi
82 schema:value 10.1007/978-3-319-06200-6_4
83 rdf:type schema:PropertyValue
84 N75d2cf07b61149b8b673ae9d30cbd501 schema:isbn 978-3-319-06199-3
85 978-3-319-06200-6
86 schema:name NASA Formal Methods
87 rdf:type schema:Book
88 N935e2c8256b3459c9656f32233621bbb schema:name Springer Nature - SN SciGraph project
89 rdf:type schema:Organization
90 Nbdaf447efa7b4b01a729968654be1926 schema:familyName Badger
91 schema:givenName Julia M.
92 rdf:type schema:Person
93 Nceac301110d84c9999c22d82f5f9931b rdf:first Ne345c1ca1663476493652ceb82c6b745
94 rdf:rest rdf:nil
95 Nd3d53b3e8abc46e5963f9a568f09aefc schema:name dimensions_id
96 schema:value pub.1042087635
97 rdf:type schema:PropertyValue
98 Ne345c1ca1663476493652ceb82c6b745 schema:familyName Rozier
99 schema:givenName Kristin Yvonne
100 rdf:type schema:Person
101 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
102 schema:name Information and Computing Sciences
103 rdf:type schema:DefinedTerm
104 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
105 schema:name Computation Theory and Mathematics
106 rdf:type schema:DefinedTerm
107 sg:person.010574656021.33 schema:affiliation grid-institutes:grid.6936.a
108 schema:familyName Rizkallah
109 schema:givenName Christine
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010574656021.33
111 rdf:type schema:Person
112 sg:person.011500152103.44 schema:affiliation grid-institutes:grid.6936.a
113 schema:familyName Noschinski
114 schema:givenName Lars
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011500152103.44
116 rdf:type schema:Person
117 sg:person.011757371347.43 schema:affiliation grid-institutes:grid.419528.3
118 schema:familyName Mehlhorn
119 schema:givenName Kurt
120 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011757371347.43
121 rdf:type schema:Person
122 grid-institutes:grid.419528.3 schema:alternateName Max-Planck-Institut für Informatik, Saarbrücken, Germany
123 schema:name Max-Planck-Institut für Informatik, Saarbrücken, Germany
124 rdf:type schema:Organization
125 grid-institutes:grid.6936.a schema:alternateName Institut für Informatik, Technische Universität München, Germany
126 schema:name Institut für Informatik, Technische Universität München, Germany
127 rdf:type schema:Organization
 




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


...