Verification of Certifying Computations View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2011

AUTHORS

Eyad Alkassar , Sascha Böhme , Kurt Mehlhorn , Christine Rizkallah

ABSTRACT

Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current verification tools and proving their correctness usually involves non-trivial mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm – yet it is all the user has to trust. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted. In this paper we develop a framework to seamlessly verify certifying computations. The automatic verifier VCC is used for checking code correctness, and the interactive theorem prover Isabelle/HOL targets high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of a typical example of the algorithmic library LEDA. More... »

PAGES

67-82

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-22110-1_7

DOI

http://dx.doi.org/10.1007/978-3-642-22110-1_7

DIMENSIONS

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


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/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/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Universit\u00e4t des Saarlandes, Germany", 
          "id": "http://www.grid.ac/institutes/grid.11749.3a", 
          "name": [
            "Universit\u00e4t des Saarlandes, Germany"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Alkassar", 
        "givenName": "Eyad", 
        "id": "sg:person.014453456327.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014453456327.46"
        ], 
        "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": "B\u00f6hme", 
        "givenName": "Sascha", 
        "id": "sg:person.011706336725.77", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011706336725.77"
        ], 
        "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"
      }, 
      {
        "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": "Rizkallah", 
        "givenName": "Christine", 
        "id": "sg:person.010574656021.33", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010574656021.33"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2011", 
    "datePublishedReg": "2011-01-01", 
    "description": "Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current verification tools and proving their correctness usually involves non-trivial mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm \u2013 yet it is all the user has to trust. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted. In this paper we develop a framework to seamlessly verify certifying computations. The automatic verifier VCC is used for checking code correctness, and the interactive theorem prover Isabelle/HOL targets high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of a typical example of the algorithmic library LEDA.", 
    "editor": [
      {
        "familyName": "Gopalakrishnan", 
        "givenName": "Ganesh", 
        "type": "Person"
      }, 
      {
        "familyName": "Qadeer", 
        "givenName": "Shaz", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-22110-1_7", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-22109-5", 
        "978-3-642-22110-1"
      ], 
      "name": "Computer Aided Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "current verification tools", 
      "Isabelle/HOL", 
      "formal verification", 
      "verification tools", 
      "interactive theorem", 
      "code correctness", 
      "complex algorithms", 
      "original algorithm", 
      "current tools", 
      "algorithm", 
      "checker", 
      "verification", 
      "computation", 
      "correctness", 
      "mathematical theorems", 
      "users", 
      "HOL", 
      "tool", 
      "typical example", 
      "mathematical properties", 
      "implementation", 
      "framework", 
      "LEDA", 
      "output", 
      "art", 
      "effectiveness", 
      "VCC", 
      "theorem", 
      "example", 
      "state", 
      "witness", 
      "addition", 
      "properties", 
      "approach", 
      "paper"
    ], 
    "name": "Verification of Certifying Computations", 
    "pagination": "67-82", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1012209895"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-22110-1_7"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-22110-1_7", 
      "https://app.dimensions.ai/details/publication/pub.1012209895"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-10-01T06:52", 
    "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_102.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-22110-1_7"
  }
]
 

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-642-22110-1_7'

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-642-22110-1_7'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-22110-1_7'

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-642-22110-1_7'


 

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

134 TRIPLES      22 PREDICATES      62 URIs      53 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-22110-1_7 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0803
5 schema:author N9372e2dbdcbf45c3a5ce317d9dd0bc24
6 schema:datePublished 2011
7 schema:datePublishedReg 2011-01-01
8 schema:description Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current verification tools and proving their correctness usually involves non-trivial mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm – yet it is all the user has to trust. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted. In this paper we develop a framework to seamlessly verify certifying computations. The automatic verifier VCC is used for checking code correctness, and the interactive theorem prover Isabelle/HOL targets high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of a typical example of the algorithmic library LEDA.
9 schema:editor N789140b4083f47e89858f122d52baf1a
10 schema:genre chapter
11 schema:isAccessibleForFree true
12 schema:isPartOf Nd9dc70634e154ac294509aa929a55deb
13 schema:keywords HOL
14 Isabelle/HOL
15 LEDA
16 VCC
17 addition
18 algorithm
19 approach
20 art
21 checker
22 code correctness
23 complex algorithms
24 computation
25 correctness
26 current tools
27 current verification tools
28 effectiveness
29 example
30 formal verification
31 framework
32 implementation
33 interactive theorem
34 mathematical properties
35 mathematical theorems
36 original algorithm
37 output
38 paper
39 properties
40 state
41 theorem
42 tool
43 typical example
44 users
45 verification
46 verification tools
47 witness
48 schema:name Verification of Certifying Computations
49 schema:pagination 67-82
50 schema:productId N211344ec71d243af8a2c65693b113c07
51 Nfa352fa02d2a44b28c5ce9a52f267e7b
52 schema:publisher Nc384f7475a6c48f59eea5bb46241f6e7
53 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012209895
54 https://doi.org/10.1007/978-3-642-22110-1_7
55 schema:sdDatePublished 2022-10-01T06:52
56 schema:sdLicense https://scigraph.springernature.com/explorer/license/
57 schema:sdPublisher Na67cc876aec24775bc1878d600a24c43
58 schema:url https://doi.org/10.1007/978-3-642-22110-1_7
59 sgo:license sg:explorer/license/
60 sgo:sdDataset chapters
61 rdf:type schema:Chapter
62 N02fd565dfdc64e4986699e573c5eac86 rdf:first sg:person.011706336725.77
63 rdf:rest Nef75a68b6bd848abbcc4315a3597e469
64 N211344ec71d243af8a2c65693b113c07 schema:name dimensions_id
65 schema:value pub.1012209895
66 rdf:type schema:PropertyValue
67 N2de9ea9f2f434389834552382e943353 rdf:first Nf589e43ed5794974b316c6bdc60c83d7
68 rdf:rest rdf:nil
69 N2df27631d484440a9820f6d4d4d00e05 rdf:first sg:person.010574656021.33
70 rdf:rest rdf:nil
71 N789140b4083f47e89858f122d52baf1a rdf:first N9afe2ed9d2ba4fe5a8979ede0b678054
72 rdf:rest N2de9ea9f2f434389834552382e943353
73 N9372e2dbdcbf45c3a5ce317d9dd0bc24 rdf:first sg:person.014453456327.46
74 rdf:rest N02fd565dfdc64e4986699e573c5eac86
75 N9afe2ed9d2ba4fe5a8979ede0b678054 schema:familyName Gopalakrishnan
76 schema:givenName Ganesh
77 rdf:type schema:Person
78 Na67cc876aec24775bc1878d600a24c43 schema:name Springer Nature - SN SciGraph project
79 rdf:type schema:Organization
80 Nc384f7475a6c48f59eea5bb46241f6e7 schema:name Springer Nature
81 rdf:type schema:Organisation
82 Nd9dc70634e154ac294509aa929a55deb schema:isbn 978-3-642-22109-5
83 978-3-642-22110-1
84 schema:name Computer Aided Verification
85 rdf:type schema:Book
86 Nef75a68b6bd848abbcc4315a3597e469 rdf:first sg:person.011757371347.43
87 rdf:rest N2df27631d484440a9820f6d4d4d00e05
88 Nf589e43ed5794974b316c6bdc60c83d7 schema:familyName Qadeer
89 schema:givenName Shaz
90 rdf:type schema:Person
91 Nfa352fa02d2a44b28c5ce9a52f267e7b schema:name doi
92 schema:value 10.1007/978-3-642-22110-1_7
93 rdf:type schema:PropertyValue
94 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
95 schema:name Information and Computing Sciences
96 rdf:type schema:DefinedTerm
97 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
98 schema:name Artificial Intelligence and Image Processing
99 rdf:type schema:DefinedTerm
100 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
101 schema:name Computation Theory and Mathematics
102 rdf:type schema:DefinedTerm
103 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
104 schema:name Computer Software
105 rdf:type schema:DefinedTerm
106 sg:person.010574656021.33 schema:affiliation grid-institutes:grid.419528.3
107 schema:familyName Rizkallah
108 schema:givenName Christine
109 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010574656021.33
110 rdf:type schema:Person
111 sg:person.011706336725.77 schema:affiliation grid-institutes:grid.6936.a
112 schema:familyName Böhme
113 schema:givenName Sascha
114 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011706336725.77
115 rdf:type schema:Person
116 sg:person.011757371347.43 schema:affiliation grid-institutes:grid.419528.3
117 schema:familyName Mehlhorn
118 schema:givenName Kurt
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011757371347.43
120 rdf:type schema:Person
121 sg:person.014453456327.46 schema:affiliation grid-institutes:grid.11749.3a
122 schema:familyName Alkassar
123 schema:givenName Eyad
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014453456327.46
125 rdf:type schema:Person
126 grid-institutes:grid.11749.3a schema:alternateName Universität des Saarlandes, Germany
127 schema:name Universität des Saarlandes, Germany
128 rdf:type schema:Organization
129 grid-institutes:grid.419528.3 schema:alternateName Max-Planck-Institut für Informatik, Saarbrücken, Germany
130 schema:name Max-Planck-Institut für Informatik, Saarbrücken, Germany
131 rdf:type schema:Organization
132 grid-institutes:grid.6936.a schema:alternateName Institut für Informatik, Technische Universität München, Germany
133 schema:name Institut für Informatik, Technische Universität München, Germany
134 rdf:type schema:Organization
 




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


...