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
Peer-reviewPublication Information
Output type
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 164-170 (7 pages)Publication milestones
- Published - 26/09/2017
Publication status
Published - 26/09/2017
Publisher
Association for Computing Machinery, United StatesBook series
- Book series name: Lecture Notes in Computer Science
Publication IDs
- Scopus: 85029502346
Host publication title
Interactive Theorem Proving: 8th International ConferenceAbstract
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.
Access to documents
Related Event
Title
International Conference on Interactive Theorem Proving
Event type
ConferenceDegree of recognition
National eventDate
26/09/2017 - 29/09/2017Location
BrasíliaBrazil