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

Department of Mathematics and Computer Science

Research output: Chapter in Book/Report/Conference proceeding › 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	Proceedings of the 8th International Conference on Interactive Theorem Proving
Editors	Mauricio Ayala-Rincón, César A. Muñoz
Publisher	Springer
Publication date	2017
Pages	164-170
ISBN (Print)	978-3-319-66106-3
ISBN (Electronic)	978-3-319-66107-0
DOIs	https://doi.org/10.1007/978-3-319-66107-0_11
Publication status	Published - 2017
Event	8th International Conference on Interactive Theorem Proving - Brasília, Brazil Duration: 26. Sept 2017 → 29. Sept 2017 Conference number: 8

Conference

Conference	8th International Conference on Interactive Theorem Proving
Number	8
Country/Territory	Brazil
City	Brasília
Period	26/09/2017 → 29/09/2017

Series	Lecture Notes in Computer Science
Volume	10499
ISSN	0302-9743

Documents & Links

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

Cite this

@inproceedings{23f0447bc67e46cf9e8d5619d48c49b6,

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

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

year = "2017",

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

language = "English",

isbn = "978-3-319-66106-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "164--170",

editor = "Mauricio Ayala-Rinc{\'o}n and Mu{\~n}oz, {C{\'e}sar A.}",

booktitle = "Proceedings of the 8th International Conference on Interactive Theorem Proving",

address = "Germany",

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

}

Cruz-Filipe, L , Larsen, KS & Schneider-Kamp, P 2017, How to Get More Out of Your Oracles. in M Ayala-Rincón & CA Muñoz (eds), Proceedings of the 8th International Conference on Interactive Theorem Proving. Springer, Lecture Notes in Computer Science, vol. 10499, pp. 164-170, 8th 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.

Proceedings of the 8th International Conference on Interactive Theorem Proving. ed. / Mauricio Ayala-Rincón; César A. Muñoz. Springer, 2017. p. 164-170 (Lecture Notes in Computer Science, Vol. 10499).

Research output: Chapter in Book/Report/Conference proceeding › 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: 8

PY - 2017

Y1 - 2017

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.

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

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

M3 - Article in proceedings

SN - 978-3-319-66106-3

T3 - Lecture Notes in Computer Science

SP - 164

EP - 170

BT - Proceedings of the 8th International Conference on Interactive Theorem Proving

A2 - Ayala-Rincón, Mauricio

A2 - Muñoz, César A.

PB - Springer

T2 - 8th 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

Documents & Links

Fingerprint

Cite this