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

University of Southern Denmark

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › 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.

Original language	English
Title of host publication	Interactive Theorem Proving: 8th International Conference
Number of pages	7
Publisher	Association for Computing Machinery
Publication date	26 Sept 2017
Pages	164-170
DOIs	https://doi.org/10.1007/978-3-319-66107-0_11
Publication status	Published - 26 Sept 2017
Externally published	Yes
Event	International Conference on Interactive Theorem Proving - Brasília, Brazil Duration: 26 Sept 2017 → 29 Sept 2017 Conference number: 8th https://doi.org/10.1007/978-3-319-66107-0

Conference

Conference	International Conference on Interactive Theorem Proving
Number	8th
Country/Territory	Brazil
City	Brasília
Period	26/09/2017 → 29/09/2017
Internet address	https://doi.org/10.1007/978-3-319-66107-0

Series	Lecture Notes in Computer Science

Keywords

formal verification
oracle-based verification
certified checkers
separation of concerns
algorithm optimization

Access to Document

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

Cite this

@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",

publisher = "Association for Computing Machinery",

pages = "164--170",

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

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. in Interactive Theorem Proving: 8th International Conference. Association for Computing Machinery, Lecture Notes in Computer Science, pp. 164-170, International Conference on Interactive Theorem Proving, Brasília, Brazil, 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. p. 164-170 (Lecture Notes in Computer Science).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › 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

Conference

Keywords

Access to Document

Fingerprint

Cite this