How to Get More Out of Your Oracles

Luís Cruz-Filipe; Kim Skak Larsen; Peter Schneider-Kamp

doi:10.1007/978-3-319-66107-0_11

How to Get More Out of Your Oracles

Luís Cruz-Filipe
, Kim Skak Larsen
, Peter Schneider-Kamp

Syddansk Universitet

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

Abstract

Formal verification of large computer-generated proofs often relies on certified checkers based on oracles. We propose a methodology for such proofs, advocating a separation of concerns between formalizing the underlying theory and optimizing the algorithm implemented in the checker, based on the observation that such optimizations can benefit significantly from adequately adapting the oracle.

Originalsprog	Engelsk
Titel	Interactive Theorem Proving: 8th International Conference
Antal sider	7
Forlag	Association for Computing Machinery
Publikationsdato	26 sep. 2017
Sider	164-170
DOI	https://doi.org/10.1007/978-3-319-66107-0_11
Status	Udgivet - 26 sep. 2017
Udgivet eksternt	Ja
Begivenhed	International Conference on Interactive Theorem Proving - Brasília, Brasilien Varighed: 26 sep. 2017 → 29 sep. 2017 Konferencens nummer: 8th https://doi.org/10.1007/978-3-319-66107-0

Konference

Konference	International Conference on Interactive Theorem Proving
Nummer	8th
Land/Område	Brasilien
By	Brasília
Periode	26/09/2017 → 29/09/2017
Internetadresse	https://doi.org/10.1007/978-3-319-66107-0

Navn	Lecture Notes in Computer Science

Adgang til dokumentet

10.1007/978-3-319-66107-0_11

Citationsformater

@inproceedings{c1fd675e0e8c4b2a9abeaa24636e61f0,

title = "How to Get More Out of Your Oracles",

abstract = "Formal verification of large computer-generated proofs often relies on certified checkers based on oracles. We propose a methodology for such proofs, advocating a separation of concerns between formalizing the underlying theory and optimizing the algorithm implemented in the checker, based on the observation that such optimizations can benefit significantly from adequately adapting the oracle.",

keywords = "formal verification, oracle-based verification, certified checkers, separation of concerns, algorithm optimization",

author = "Lu{\'i}s Cruz-Filipe and Larsen, \{Kim Skak\} and Peter Schneider-Kamp",

note = "8th International Conference on Interactive Theorem Proving, ITP 2017 ; Conference date: 26-09-2017 Through 29-09-2017; International Conference on Interactive Theorem Proving, ITP ; Conference date: 26-09-2017 Through 29-09-2017",

year = "2017",

month = sep,

day = "26",

doi = "10.1007/978-3-319-66107-0\_11",

language = "English",

series = "Lecture Notes in Computer Science",

pages = "164--170",

booktitle = "Interactive Theorem Proving: 8th International Conference",

publisher = "Association for Computing Machinery",

address = "United States",

url = "https://doi.org/10.1007/978-3-319-66107-0",

}

Cruz-Filipe, L, Larsen, KS & Schneider-Kamp, P 2017, How to Get More Out of Your Oracles. i Interactive Theorem Proving: 8th International Conference. Association for Computing Machinery, Lecture Notes in Computer Science, s. 164-170, International Conference on Interactive Theorem Proving, Brasília, Brasilien, 26/09/2017. https://doi.org/10.1007/978-3-319-66107-0_11

How to Get More Out of Your Oracles. / Cruz-Filipe, Luís; Larsen, Kim Skak; Schneider-Kamp, Peter.
Interactive Theorem Proving: 8th International Conference. Association for Computing Machinery, 2017. s. 164-170 (Lecture Notes in Computer Science).

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - How to Get More Out of Your Oracles

AU - Cruz-Filipe, Luís

AU - Larsen, Kim Skak

AU - Schneider-Kamp, Peter

N1 - Conference code: 8th

PY - 2017/9/26

Y1 - 2017/9/26

N2 - Formal verification of large computer-generated proofs often relies on certified checkers based on oracles. We propose a methodology for such proofs, advocating a separation of concerns between formalizing the underlying theory and optimizing the algorithm implemented in the checker, based on the observation that such optimizations can benefit significantly from adequately adapting the oracle.

AB - Formal verification of large computer-generated proofs often relies on certified checkers based on oracles. We propose a methodology for such proofs, advocating a separation of concerns between formalizing the underlying theory and optimizing the algorithm implemented in the checker, based on the observation that such optimizations can benefit significantly from adequately adapting the oracle.

KW - formal verification

KW - oracle-based verification

KW - certified checkers

KW - separation of concerns

KW - algorithm optimization

U2 - 10.1007/978-3-319-66107-0_11

DO - 10.1007/978-3-319-66107-0_11

M3 - Article in proceedings

T3 - Lecture Notes in Computer Science

SP - 164

EP - 170

BT - Interactive Theorem Proving: 8th International Conference

PB - Association for Computing Machinery

T2 - International Conference on Interactive Theorem Proving

Y2 - 26 September 2017 through 29 September 2017

ER -

How to Get More Out of Your Oracles

Abstract

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater